Theories, solvers and static analysis by abstract interpretation

Patrick Cousot, Radhia Cousot, Laurent Mauborgne

Research output: Contribution to journalArticlepeer-review


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).

Original languageEnglish (US)
Article number31
JournalJournal of the ACM
Issue number6
StatePublished - Dec 2012


  • Decision procedures
  • Interpretation
  • Program logics
  • Program verification
  • Sat modulo theory
  • Semantics
  • Smt solver
  • Static analysis
  • Theorem proving

ASJC Scopus subject areas

  • Software
  • Control and Systems Engineering
  • Information Systems
  • Hardware and Architecture
  • Artificial Intelligence


Dive into the research topics of 'Theories, solvers and static analysis by abstract interpretation'. Together they form a unique fingerprint.

Cite this