Combining Algebraic Domains and Logical Theories by the Reduced Product.
Invited Talk, 18th International Static Analysis Symposium, SAS 2011, September 14th-16th, 2011.
In static analysis by abstract interpretation, algebraic abstract domains can be combined by the reduced product, or over-approximated by the iterated pairwise reductions.
In Satisfiability Modulo Theories (SMT) solvers, the Nelson-Oppen (NO) theory combination schema provides, under various restrictions, a sound and complete decision procedure for combining disjoint theories by exchanges of disjunctions of equalities and disequalities. Understanding theories as abstract domains, we show that the NO procedure is an iterated pairwise reduction (which is comple hence a reduced product).
In the context of static analysis, completeness is useless in the abstract since the static analysis problem is undecidable anyway. This point of view introduces generalizations which, when combined with bounded widenings (such as interpolation), yields new cominations of algebraic and logical abstractions.
Joint work with Radhia Cousot, ENS & CNRS, Paris and Laurent Mauborgne, IMDEA, Madrid.
\bibitem{Cousot-SAS-2011-09-14}
P. Cousot.
\newblock Combining Algebraic Domains and Logical Theories by the Reduced Product (joint work with R. Cousot and L. Mauborgne).
\newblock \emph{Invited talk}, Static Analysis Symposium, SAS 2011, Venezia, Italy.
14 September 2011.
@inProceedings{Cousot-SAS-2011-09-14,
author = {P{.} Cousot},
title = {Combining Algebraic Domains and Logical Theories by the Reduced Product (joint work with R. Cousot and L. Mauborgne)},
booktitle = {Invited talk, Static Analysis Symposium, SAS 2011},
address = {Venezia, Italy},
month = {14 September},
year = {2011},
}
 |
 |
| Ca' Dolfin | Ca' Foscari |
 |
 |
| Ca' Foscari | Bridge from Ca' Dolfin to Ca' Foscari |
 |
 |
| SAS 2011 conference room in Ca' Dolfin | SAS 2011 conference room in Ca' Dolfin |
 |
 |
| Breaks in Ca' Dolfin | Breaks in Ca' Dolfin |
 |
 |
| SASB 2011 Conference room in Ca' Foscari | Canal grande from Ca' Foscari |
 |
 |
| Canal grande from Ca' Foscari | Canal grande from Ca' Foscari |
 |
 |
| Ensemble DVLCIS IN FVNDO: Giulia Pattaro (soprano) - Andrea Marcialis (recorders) | Stephano Sopranzi (baroque basson) - Luca Poppi (harpsichord) |
 |
|
| Baroque ensemble on original instruments |