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. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Cousot, P., Cousot, R., & Mauborgne, L. (2011). Logical abstract domains and interpretations. In The Future of Software Engineering (pp. 48–71). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-15187-3_3
Mendeley helps you to discover research relevant for your work.