Theories, Solvers and Static Analysis by Abstract Interpretation


August 12, 2011


Patrick Cousot and Radhia Cousot


Ecole Normale Superieure


The algebraic/model theoretic design of static analyzers uses abstract domains based on representations of properties and pre-calculated property transformers. It is very efficient. The logical/proof theoretic approach uses SMT solvers/theorem provers and computation of property transformers on-the-fly. It is very expressive. We propose to unify both approaches, so that they can be combined to reach the sweet spot best adapted to a specific application domain in the precision/cost spectrum. We first give a new formalization of the proof theoretic approach in the abstract interpretation framework, introducing a semantics based on multiple interpretations to deal with the soundness of such approaches. Then we describe how to combine them with any other abstract interpretation-based analysis using an iterated reduction to combine abstractions. The key observation is that the Nelson-Oppen procedure which decides satisfiability in a combination of logical theories by exchanging equalities and disequalities computes a reduced product (after the state is enhanced with some new “observations” corresponding to alien terms). By abandoning restrictions ensuring completeness (such as disjointness, convexity, stably-infiniteness, or shininess, etc) we can even broaden the application scope of logical abstractions for static analysis (which is incomplete anyway). Joint work with Laurent Mauborgne (IMDEA, Madrid)


Patrick Cousot and Radhia Cousot

Patrick Cousot received his PhD in 1978 from the University Joseph Fourier of Grenoble, France. He his presently professor of computer science at the Ecole Normale Supérieure in Paris. His main research interest is software verification. His main contribution is “abstract interpretation”, a set-theoretic theory of approximation which has been applied to the semantics of programming languages, static program checking, abstract model checking, etc.