P. Cousot, Unifying proof theoretic/logical and algebraic abstractions for inference and verification

Patrick Cousot (work with Radhia Cousot and Laurent Mauborgne).
Unifying proof theoretic/logical and algebraic abstractions for inference and verification.
CMACS-NSF Meeting, University of Maryland, College Park, MD, USA. April 28^th-29^th, 2011.
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 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). We also introduce a semantics based on multiple interpretations to deal with the soundness of that combinations on a formal basis.
Slides of the 30 mn presentation (to be used with Acrobat Reader): .pdf.

Bibliographic reference:

\bibitem{Cousot-CMACS-2011-04-28--29}
P.~Cousot.
\newblock Unifying proof theoretic/logical and algebraic abstractions for inference and verification.
\newblock \emph{CMACS-NSF Meeting}, University of Maryland, College Park, MD, USA.
          28--29 April 2011.

@inProceedings{Cousot-CMACS-2011-04-28--29,
   author =    {P{.} Cousot},
   title =     {Unifying proof theoretic/logical and algebraic abstractions for inference and verification},
   booktitle = {CMACS-NSF Meeting},
   address =   {University of Maryland, College Park, MD, USA.},
   month =     {28--29 April},
   year =      {2011},
}

Copyright notice
Last modified: Monday, 07-May-2012 17:51:02 EDT