The Reduced Product of Abstract Domains and the Combination of Decision Procedures

Patrick Cousot, Radhia Cousot, Jérôme Feret and Laurent Mauborgne.
The Reduced Product of Abstract Domains and the Combination of Decision Procedures.
In Martin Hofmann, editor, Foundations of Software and Computational Structures (FOSSACS 2011), volume 6604 of Lecture Notes in Computer Science, pages 456--472.
Springer-Verlag, 2011.
download.
Abstract: The algebraic/model theoretic design of static analyzers uses abstract domains based on efficient representations of properties and pre-calculated property transformers. It is very efficient. The logical/proof theoretic approach uses SMT solvers and computation on-the-fly of property transformers. It is very expressive. We propose a combination of the two approaches to reach the sweet spot best adapted to a specific application domain in the precision/cost spectrum. The proposed combination uses 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 by undecidability). We also introduce a semantics based on multiple interpretations to deal with the soundness of that combinations on a formal basis.

\bibitem{ccm11}
Patrick Cousot, Radhia Cousot, and Laurent Mauborgne.
\newblock The reduced product of abstract domains and the combination of
  decision procedures.
\newblock In M.~Hofmann, editor, {\em 14th International Conference on
  Fondations of Software Science and Computation Structures (FoSSaCS 2011)},
  volume 6604 of {\em Lecture Notes in Computer Science}, pages 456--472.
  Springer-Verlag, 2011.



@inproceedings{ccm11,
author = "Patrick Cousot and Radhia Cousot and Laurent Mauborgne",
title = "The reduced product of abstract domains and the combination of decision procedures",
booktitle = "14th International Conference on Fondations of Software Science and Computation Structures (FoSSaCS 2011)",
volume = 6604,
series = "Lecture Notes in Computer Science",
year = 2011,
publisher = "Springer-Verlag",
editor = "M. Hofmann",
pages = "456--472",
}

Email: Laurent.Mauborgne@imdea.org