Abstract:
We give semantic foundations to abstract domains consisting in first
order logic formulæ in a theory, as used in verification tools or methods using
SMT-solvers or theorem provers.We exhibit conditions for a sound usage of such
methods with respect to multi-interpreted semantics and extend their usage to
automatic invariant generation by abstract interpretation.
\bibitem[CCM10a]{ccm10-b}
Patrick Cousot, Radhia Cousot, and Laurent Mauborgne.
\newblock Logical abstract domains and interpretations.
\newblock In S.~Nanz, editor, {\em The Future of Software Engineering}, pages
48--71. Springer-Verlag, Heidelberg, 2011.
@incollection{ccm10-b,
author = "Patrick Cousot and Radhia Cousot and Laurent Mauborgne",
title = "Logical Abstract Domains and Interpretations",
booktitle = "The Future of Software Engineering",
editor = "S. Nanz",
publisher = "Springer-Verlag",
address = "Heidelberg",
pages = "48--71",
year = 2011,
}