Frameworks for abstract interpretation

Research output: Contribution to journalArticleResearchpeer-review

22 Citations (Scopus)

Abstract

Abstract interpretation theory provides a semantic foundation for dataflow analysis of programs by formalizing the relationship between analysis and semantics. In the original theory for abstract interpretation, due to Cousot and Cousot, this relationship was given in terms of an adjoined pair of functions. One function, called the abstraction function, mapped data to their best description, while the second function, called the concretization function, mapped descriptions to the largest data object they described. Since this time, however, a number of other "frameworks" for abstract interpretation have been developed, differing in how the descriptions are related to the actual data used in computation. For instance, one framework uses only abstraction functions, another uses only concretization functions, while yet another allows an arbitrary approximation relation. We illustrate that each of these frameworks has certain advantages and limitations. This motivates our development and study of a general framework which encompasses these other approaches. We examine this framework with regard to three questions: when does approximation lift from base functions to all expressions; when is approximation transitive; and when is there an optimal approximation and how can it be inferred? Answers to these questions are not only interesting in the context of our framework but also provide a better understanding of the other frameworks.

Original languageEnglish
Pages (from-to)103-129
Number of pages27
JournalActa Informatica
Volume30
Issue number2
DOIs
Publication statusPublished - 1 Feb 1993

Cite this

Marriott, Kim. / Frameworks for abstract interpretation. In: Acta Informatica. 1993 ; Vol. 30, No. 2. pp. 103-129.
@article{b1e8cde46d3e47a3a87292031b3d0e7e,
title = "Frameworks for abstract interpretation",
abstract = "Abstract interpretation theory provides a semantic foundation for dataflow analysis of programs by formalizing the relationship between analysis and semantics. In the original theory for abstract interpretation, due to Cousot and Cousot, this relationship was given in terms of an adjoined pair of functions. One function, called the abstraction function, mapped data to their best description, while the second function, called the concretization function, mapped descriptions to the largest data object they described. Since this time, however, a number of other {"}frameworks{"} for abstract interpretation have been developed, differing in how the descriptions are related to the actual data used in computation. For instance, one framework uses only abstraction functions, another uses only concretization functions, while yet another allows an arbitrary approximation relation. We illustrate that each of these frameworks has certain advantages and limitations. This motivates our development and study of a general framework which encompasses these other approaches. We examine this framework with regard to three questions: when does approximation lift from base functions to all expressions; when is approximation transitive; and when is there an optimal approximation and how can it be inferred? Answers to these questions are not only interesting in the context of our framework but also provide a better understanding of the other frameworks.",
author = "Kim Marriott",
year = "1993",
month = "2",
day = "1",
doi = "10.1007/BF01178576",
language = "English",
volume = "30",
pages = "103--129",
journal = "Acta Informatica",
issn = "0001-5903",
publisher = "Springer-Verlag London Ltd.",
number = "2",

}

Frameworks for abstract interpretation. / Marriott, Kim.

In: Acta Informatica, Vol. 30, No. 2, 01.02.1993, p. 103-129.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - Frameworks for abstract interpretation

AU - Marriott, Kim

PY - 1993/2/1

Y1 - 1993/2/1

N2 - Abstract interpretation theory provides a semantic foundation for dataflow analysis of programs by formalizing the relationship between analysis and semantics. In the original theory for abstract interpretation, due to Cousot and Cousot, this relationship was given in terms of an adjoined pair of functions. One function, called the abstraction function, mapped data to their best description, while the second function, called the concretization function, mapped descriptions to the largest data object they described. Since this time, however, a number of other "frameworks" for abstract interpretation have been developed, differing in how the descriptions are related to the actual data used in computation. For instance, one framework uses only abstraction functions, another uses only concretization functions, while yet another allows an arbitrary approximation relation. We illustrate that each of these frameworks has certain advantages and limitations. This motivates our development and study of a general framework which encompasses these other approaches. We examine this framework with regard to three questions: when does approximation lift from base functions to all expressions; when is approximation transitive; and when is there an optimal approximation and how can it be inferred? Answers to these questions are not only interesting in the context of our framework but also provide a better understanding of the other frameworks.

AB - Abstract interpretation theory provides a semantic foundation for dataflow analysis of programs by formalizing the relationship between analysis and semantics. In the original theory for abstract interpretation, due to Cousot and Cousot, this relationship was given in terms of an adjoined pair of functions. One function, called the abstraction function, mapped data to their best description, while the second function, called the concretization function, mapped descriptions to the largest data object they described. Since this time, however, a number of other "frameworks" for abstract interpretation have been developed, differing in how the descriptions are related to the actual data used in computation. For instance, one framework uses only abstraction functions, another uses only concretization functions, while yet another allows an arbitrary approximation relation. We illustrate that each of these frameworks has certain advantages and limitations. This motivates our development and study of a general framework which encompasses these other approaches. We examine this framework with regard to three questions: when does approximation lift from base functions to all expressions; when is approximation transitive; and when is there an optimal approximation and how can it be inferred? Answers to these questions are not only interesting in the context of our framework but also provide a better understanding of the other frameworks.

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

U2 - 10.1007/BF01178576

DO - 10.1007/BF01178576

M3 - Article

VL - 30

SP - 103

EP - 129

JO - Acta Informatica

JF - Acta Informatica

SN - 0001-5903

IS - 2

ER -