Patrick Cousot, Radhia Cousot, & Laurent Mauborgne.<bR> A Galois connection calculus for abstract interpretation.

Patrick Cousot, Radhia Cousot, & Laurent Mauborgne .
Theories, solvers and static analysis by abstract interpretation.
In Journal of the Association for Computing Machinery 59(6), 31 p., 2012. © ACM Press, New York.
Letter paper format: Paper (PDF, 472 Kb)
Abstract:
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).
Categories and Subject Descriptors:
D.2.4 [Software Engineering/Program Verification/Formal methods, validation, assertion checkers];
D.3.1 [Programming Languages/Formal Definitions and Theory/Semantics];
F.3.1 [Logics and Meanings of Programs/Specifying and Verifying and Reasoning about Programs/Mechanical verification, assertions, invariants];
F.3.2 [Logics and Meaning of Programs/Semantics of Programming Languages/Program analysis].
General Terms: Languages, Performance, Reliability, Theory, Verification.
Keywords: Abstract Interpretation, Decision Procedures, Program Logics, Program Verification, SAT Modulo Theory, SMT solver, Semantics, Static Analysis, Theorem Proving.

Bibliographic reference:

\bibitem{CousotCousotMauborgne-JACM12}
P.~Cousot, R.~Cousot, \& L.~Mauborgne.
\newblock Theories, solvers and static analysis by abstract interpretation.
\newblock In \emph{J. ACM}, 59(6), 31 p. 2012. ACM Press, New York, NY.

@inproceedings{CousotCousotMauborgne-JACM12,
  author    = {Patrick Cousot and
               Radhia Cousot and
               Laurent Mauborgne},
  title     = {Theories, solvers and static analysis by abstract interpretation},
  journal   = {J.~ACM},
  volume    = {59},
  number    = {6},
  year      = {2012},
  pages     = {31},
  ee        = {http://doi.acm.org/10.1145/2395116.2395120},
}

Copyright: © ACM, (2014). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in J. ACM, 59(6), 2012. Copyright © 2014 ACM

copyright notice, ACM copyright
Last modified: Mon May 12 13:40:32 EDT 2014