Logical abstract domains and interpretations

Patrick Cousot, Radhia Cousot, Laurent Mauborgne

Research output: Chapter in Book/Report/Conference proceedingChapter

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.

Original languageEnglish (US)
Title of host publicationThe Future of Software Engineering
PublisherSpringer Berlin Heidelberg
Pages48-71
Number of pages24
ISBN (Print)9783642151866
DOIs
StatePublished - 2011

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Logical abstract domains and interpretations'. Together they form a unique fingerprint.

  • Cite this

    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