Tutorial Speaker David Monniaux
David Monniaux is senior researcher (directeur de recherche) at CNRS (French national center for scientific research). He is director of Verimag, a research laboratory on software and hardware verification and validation jointly operated by CNRS and Université Grenoble Alpes in the greater Grenoble area, France.
David Monniaux defended his thesis in 2001 at Université Paris Dauphine, which considered abstract interpretation of probabilistic programs. He then worked in static analysis by abstract interpretation of safety-critical systems and was one of the developers of the Astrée static analyzer, now used by major industry such as Airbus. He then worked on topics such as SMT solving, quantifier elimination, verified computations over convex polyhedra, static analysis of programs operating over caches, decidability and complexity of analyses, and abstract interpretation of programs operating over arrays and array-like structures. Lately he has been working on formally verified optimizing compilation.
He has taught at various universities in France and abroad.
Talk
Flavors of Abstract Interpretation
Monday, 16:20
Room: Europe A
Abstract interpretation is a general framework for approximate (but correct) reasoning on programs. It is the theory behind many analyses, in automated verification tools and compilers. The classical practical view of it involves iterative solving of a system of equations, perhaps with convergence aided by widening operators. In this talk, we shall see variations on this approach.