Abstract interpretation frameworks

Patrick Cousot; Radhia Cousot

doi:10.1093/logcom/2.4.511

Abstract interpretation frameworks

Patrick Cousot, Radhia Cousot

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

We introduce abstract interpretation frameworks which are variations on the archetypal framework using Galois connections between concrete and abstract semantics, widenings and narrowings and are obtained by relaxation of the original hypotheses. We consider various ways of establishing the correctness of an abstract interpretation depending on how the relation between the concrete and abstract semantics is denned. We insist upon those correspondences allowing for the inducing of the approximate abstract semantics from the concrete one. Furthermore we study various notions of widening and narrowing as a means of obtaining convergence in the iterations used in abstract interpretation.

Original language	English (US)
Pages (from-to)	511-547
Number of pages	37
Journal	Journal of Logic and Computation
Volume	2
Issue number	4
DOIs	https://doi.org/10.1093/logcom/2.4.511
State	Published - Aug 1992

Keywords

Abstract interpretation
Abstraction
Concrete and abstract semantics
Concretization
Discrete approximation
Galois connections
Narrowing
Soundness relation
Standard and collecting semantics
Widening

ASJC Scopus subject areas

Theoretical Computer Science
Software
Arts and Humanities (miscellaneous)
Hardware and Architecture
Logic

Access to Document

10.1093/logcom/2.4.511

Cite this

@article{03d2be48073044faaffd42beacc27d3a,

title = "Abstract interpretation frameworks",

abstract = "We introduce abstract interpretation frameworks which are variations on the archetypal framework using Galois connections between concrete and abstract semantics, widenings and narrowings and are obtained by relaxation of the original hypotheses. We consider various ways of establishing the correctness of an abstract interpretation depending on how the relation between the concrete and abstract semantics is denned. We insist upon those correspondences allowing for the inducing of the approximate abstract semantics from the concrete one. Furthermore we study various notions of widening and narrowing as a means of obtaining convergence in the iterations used in abstract interpretation.",

keywords = "Abstract interpretation, Abstraction, Concrete and abstract semantics, Concretization, Discrete approximation, Galois connections, Narrowing, Soundness relation, Standard and collecting semantics, Widening",

author = "Patrick Cousot and Radhia Cousot",

note = "Funding Information: We would like to thank Alan Mycroft for numerous judicial and useful comments on a first draft of this paper as well as the anonymous referees for their constructive suggestions for improvement. This work was supported in part by Esprit BRA 3124 Semantique and CNRS PRC C3.",

year = "1992",

month = aug,

doi = "10.1093/logcom/2.4.511",

language = "English (US)",

volume = "2",

pages = "511--547",

journal = "Journal of Logic and Computation",

issn = "0955-792X",

publisher = "Oxford University Press",

number = "4",

}

TY - JOUR

T1 - Abstract interpretation frameworks

AU - Cousot, Patrick

AU - Cousot, Radhia

N1 - Funding Information: We would like to thank Alan Mycroft for numerous judicial and useful comments on a first draft of this paper as well as the anonymous referees for their constructive suggestions for improvement. This work was supported in part by Esprit BRA 3124 Semantique and CNRS PRC C3.

PY - 1992/8

Y1 - 1992/8

N2 - We introduce abstract interpretation frameworks which are variations on the archetypal framework using Galois connections between concrete and abstract semantics, widenings and narrowings and are obtained by relaxation of the original hypotheses. We consider various ways of establishing the correctness of an abstract interpretation depending on how the relation between the concrete and abstract semantics is denned. We insist upon those correspondences allowing for the inducing of the approximate abstract semantics from the concrete one. Furthermore we study various notions of widening and narrowing as a means of obtaining convergence in the iterations used in abstract interpretation.

AB - We introduce abstract interpretation frameworks which are variations on the archetypal framework using Galois connections between concrete and abstract semantics, widenings and narrowings and are obtained by relaxation of the original hypotheses. We consider various ways of establishing the correctness of an abstract interpretation depending on how the relation between the concrete and abstract semantics is denned. We insist upon those correspondences allowing for the inducing of the approximate abstract semantics from the concrete one. Furthermore we study various notions of widening and narrowing as a means of obtaining convergence in the iterations used in abstract interpretation.

KW - Abstract interpretation

KW - Abstraction

KW - Concrete and abstract semantics

KW - Concretization

KW - Discrete approximation

KW - Galois connections

KW - Narrowing

KW - Soundness relation

KW - Standard and collecting semantics

KW - Widening

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

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

U2 - 10.1093/logcom/2.4.511

DO - 10.1093/logcom/2.4.511

M3 - Article

AN - SCOPUS:0000963996

SN - 0955-792X

VL - 2

SP - 511

EP - 547

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 4

ER -

Abstract interpretation frameworks

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this