We suggest a method for incremental design and refinement of abstract interpreters combining algebraic and logical abstract domains by iterated reduction — an iterative algorithm for computing an overapproximation of a reduced product by pairwise exchange of observations between the components. The pairwise nature provides an easy way to add new components to the product abstract domain, because the only work is to define exchange of observations between the new component and each one of the previous components, separately. The analysis of each component is performed separately from other components. In particular, there is no need to define new transformers whenever a new component is added to the product, because the abstract interpreter for the product uses only the transformers of the individual components.
Moreover, when an abstract domain of logical formulas is used as one of the components, its operations can be effectively implemented using an appropriate decision procedure, e.g., SMT solver. To do so, we recast the Nelson-Oppen theory combination procedure — which decides satisfiability in a combination of logical theories — in terms of abstract interpretation by identifying it as a reduced product of logical abstract domains after the state is enhanced with some new 'observations'. In other words, the purification phase of the Nelson-Oppen procedure can be seen as adding new "observables", and then the equality exchange phase can be seen as performing iterated reduction. Unlike Nelson-Oppen procedure and its subsequent extensions and implementations, the proposed framework does not place the usual restrictions (e.g., disjointness, convexity, stably-infinite) on the components, because the component abstract domains usually do not have any completeness guarantees anyway.
The semantics of logical theories is given in terms of interpretations, so meanings are assigned to programs in terms of tuples of interpretation and valuation. Classically, the semantics of a program is given as a set of valuations of variables (reachable states), but in this paper, the meaning of a program is a set of pairs < I, v >, where v is a valuation as before and I is an "interpretation" (that assigns a meaning to the function/predicate symbols). The paper establishes soundness with respect to these new semantics.
This opens up possibilities for interesting synergies between SMT solvers and program analyzers such as combinations of logical and algebraic abstract domains, and inference of properties of programs whose semantics is defined in terms of (combinations of) theories for which no effective decision procedure exists or the consideration of both a mathematical and implementation semantics of operators of the programming language.
\bibitem{CousotCousotMauborgne-FoSSaCS-11}
Patrick Cousot, Radhia Cousot, and Laurent Mauborgne.
\newblock The reduced product of abstract domains and the combination of
decision procedures.
\newblock In 14th International Conference on Fondations of Software Science
and Computation Structures, M.~Hofmann (Ed.), March 26 -- April 3, 2011,
Saarbr{\"u}cken, Germany.
\newblock Lecture Notes in Computer Science, Vol. 6604, pages 456--472,
Springer-Verlag, Heidelberg, 2011.
@incollection{CousotCousotMauborgne-FoSSaCS-11,
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), Saarbr{\"u}cken, Germany",
editor = "M.~Hofmann",
series = "Lecture Notes in Computer Science",
volume = {6604},
publisher = "Springer-Verlag",
address = "Heidelberg",
pages = "456--472",
month = {March 26 -- April 3, },
year = 2011,
}