Seminars

Static Analysis by Abstract Interpretation of Numerical Programs and Systems, and FLUCTUAT PDF
Eric Goubault & Sylvie Putot
CEA LIST Institute / Ecole Polytechnique

4/3/2013, 1:00pm, GHC 7501

Abstract:

This talk is essentially a survey of our work over the last 10 years or so, dealing with the precise analysis of numerical programs, essentially control programs such as the ones found in the aerospace, nuclear and
automotive industry. Our approach has been based on a rather generic abstract domain, based on
"zonotopes" or "affine forms", but with some specificities. For instance, our zonotopic domain provides a
functional abstraction i.e. an abstraction of the input-output relationships between values of variables. Also, our domain deals with the real number and the finite precision (for instance, floating-point) semantics. It is used in practice in FLUCTUAT to prove some functional properties of programs, generate (counter-) examples, identify the discrepancy between the real number and the finite precision semantics and its origin etc. Many extensions of this "base" domain have been designed over the years: constrained affine forms, under-approximations, hybrid extensions and more recently, "imprecise probabilistic" analyzes, where we consider that inputs of the program under analysis can be given by (non-deterministic) ranges as well as probability or sets of probability distributions. Recently, we have also introduced a "discontinuity" analysis to deal with the potential control flow discrepancy between the real number and the finite precision semantics. If time permits, we will give some focus on some of these extensions, in particular the imprecise probabilistic one.

Biography

Eric Goubault is Ingénieur Général des Mines (high-ranking civil servant, at the Ministry of Industry), detached at the French Atomic Energy Commission (CEA) since 1998. He is director of research in theoretical computer science, and professor at Ecole Polytechnique on the Engineering of Complex Industrial Systems chair (Ecole Polytechnique-Thalès) and at Institut National des Sciences et Techniques du Nucléaire, co-responsible of a master's degree in Computer Science and Applied Mathematics. He leads since 2006 a CEA laboratory and a joint research team with CNRS and Ecole Polytechnique, both called MeASI. Prior to this detachment at CEA, he has been Chargé de Recherche au CNRS de première classe at Ecole Normale Supérieure in Patrick Cousot's abstract interpretation team (1995-1997). His research interests include algebraic topology, theoretical computer science (semantics), static analysis, abstract interpretation, concurrency theory and analysis of numerical
systems.

Sylvie Putot holds a PhD in applied mathematics (2001) and an Habilitation a Diriger des Recherches in computer science (2012). Since 2001 she joined a team at CEA Saclay specialized in static analysis by abstract interpretation. She is an expert in static analysis of numerical properties, and the
main architect of the validation tool FLUCTUAT. She is also lecturer at Ecole Polytechnique.