Logical abstract domains and interpretations

Patrick Cousot; Radhia Cousot; Laurent Mauborgne

doi:10.1007/978-3-642-15187-3_3

Logical abstract domains and interpretations

Patrick Cousot, Radhia Cousot, Laurent Mauborgne

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Chapter

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 language	English (US)
Title of host publication	The Future of Software Engineering
Publisher	Springer Berlin Heidelberg
Pages	48-71
Number of pages	24
ISBN (Print)	9783642151866
DOIs	https://doi.org/10.1007/978-3-642-15187-3_3
State	Published - 2011

ASJC Scopus subject areas

Computer Science(all)

Access to Document

10.1007/978-3-642-15187-3_3

Cite this

@inbook{772e9f8c32c94621803671425f3215fa,

title = "Logical abstract domains and interpretations",

abstract = "We give semantic foundations to abstract domains consisting in first order logic formul{\ae} 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.",

author = "Patrick Cousot and Radhia Cousot and Laurent Mauborgne",

year = "2011",

doi = "10.1007/978-3-642-15187-3_3",

language = "English (US)",

isbn = "9783642151866",

pages = "48--71",

booktitle = "The Future of Software Engineering",

publisher = "Springer Berlin Heidelberg",

}

TY - CHAP

T1 - Logical abstract domains and interpretations

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Mauborgne, Laurent

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84892307194&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84892307194&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-15187-3_3

DO - 10.1007/978-3-642-15187-3_3

M3 - Chapter

AN - SCOPUS:84892307194

SN - 9783642151866

SP - 48

EP - 71

BT - The Future of Software Engineering

PB - Springer Berlin Heidelberg

ER -

Logical abstract domains and interpretations

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this