Logical abstract domains and interpretations

Patrick Cousot, Radhia Cousot, Laurent Mauborgne

Research output: Chapter in Book/Report/Conference proceedingChapter


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
Number of pages24
ISBN (Print)9783642151866
StatePublished - 2011

ASJC Scopus subject areas

  • General Computer Science


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

Cite this