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