Complementation in abstract interpretation

Agostino Cortesi; Gilberto Filé; Roberto Giacobazzi; Catuscia Palamidessi; Francesco Ranzato

doi:10.1007/3-540-60360-3_35

Complementation in abstract interpretation

Agostino Cortesi
, Gilberto Filé
, Roberto Giacobazzi
, Catuscia Palamidessi
, Francesco Ranzato

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

11 Scopus citations

Abstract

The reduced product of abstract domains is a rather well known operation in abstract interpretation. In this paper we study the inverse operation, which we call complementation. Such an operation allows to systematically decompose domains; it provides a systematic way to design new abstract domains; it allows to simplify domain verification problems, like correctness proofs; and it yields space saving representations for domains. We show that the complement exists in most cases, and we apply complementation to two well known abstract domains, notably to the Cousot and Cousot's comportment domain for analysis of functional languages and to the complex domain Sharing for aliasing analysis of logic languages.

Original language	English (US)
Title of host publication	Static Analysis - 2nd International Symposium, SAS 1995, Proceedings
Editors	Alan Mycroft
Publisher	Springer-Verlag
Pages	100-117
Number of pages	18
ISBN (Print)	9783540603603
DOIs	https://doi.org/10.1007/3-540-60360-3_35
State	Published - 1995
Externally published	Yes
Event	2nd International Static Analysis Symposium, SAS 1995 - Glasgow, United Kingdom Duration: Sep 25 1995 → Sep 27 1995

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	983
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	2nd International Static Analysis Symposium, SAS 1995
Country/Territory	United Kingdom
City	Glasgow
Period	9/25/95 → 9/27/95

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/3-540-60360-3_35

Cite this

Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C., & Ranzato, F. (1995). Complementation in abstract interpretation. In A. Mycroft (Ed.), Static Analysis - 2nd International Symposium, SAS 1995, Proceedings (pp. 100-117). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 983). Springer-Verlag. https://doi.org/10.1007/3-540-60360-3_35

Complementation in abstract interpretation. / Cortesi, Agostino; Filé, Gilberto; Giacobazzi, Roberto et al.
Static Analysis - 2nd International Symposium, SAS 1995, Proceedings. ed. / Alan Mycroft. Springer-Verlag, 1995. p. 100-117 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 983).

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

Cortesi, A, Filé, G, Giacobazzi, R, Palamidessi, C & Ranzato, F 1995, Complementation in abstract interpretation. in A Mycroft (ed.), Static Analysis - 2nd International Symposium, SAS 1995, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 983, Springer-Verlag, pp. 100-117, 2nd International Static Analysis Symposium, SAS 1995, Glasgow, United Kingdom, 9/25/95. https://doi.org/10.1007/3-540-60360-3_35

Cortesi A, Filé G, Giacobazzi R, Palamidessi C, Ranzato F. Complementation in abstract interpretation. In Mycroft A, editor, Static Analysis - 2nd International Symposium, SAS 1995, Proceedings. Springer-Verlag. 1995. p. 100-117. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-60360-3_35

Cortesi, Agostino ; Filé, Gilberto ; Giacobazzi, Roberto et al. / Complementation in abstract interpretation. Static Analysis - 2nd International Symposium, SAS 1995, Proceedings. editor / Alan Mycroft. Springer-Verlag, 1995. pp. 100-117 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5894f15f7cd34bcbaf62375b3c4217e0,

title = "Complementation in abstract interpretation",

abstract = "The reduced product of abstract domains is a rather well known operation in abstract interpretation. In this paper we study the inverse operation, which we call complementation. Such an operation allows to systematically decompose domains; it provides a systematic way to design new abstract domains; it allows to simplify domain verification problems, like correctness proofs; and it yields space saving representations for domains. We show that the complement exists in most cases, and we apply complementation to two well known abstract domains, notably to the Cousot and Cousot's comportment domain for analysis of functional languages and to the complex domain Sharing for aliasing analysis of logic languages.",

author = "Agostino Cortesi and Gilberto Fil{\'e} and Roberto Giacobazzi and Catuscia Palamidessi and Francesco Ranzato",

year = "1995",

doi = "10.1007/3-540-60360-3\_35",

language = "English (US)",

isbn = "9783540603603",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer-Verlag",

pages = "100--117",

editor = "Alan Mycroft",

booktitle = "Static Analysis - 2nd International Symposium, SAS 1995, Proceedings",

note = "2nd International Static Analysis Symposium, SAS 1995 ; Conference date: 25-09-1995 Through 27-09-1995",

}

TY - GEN

T1 - Complementation in abstract interpretation

AU - Cortesi, Agostino

AU - Filé, Gilberto

AU - Giacobazzi, Roberto

AU - Palamidessi, Catuscia

AU - Ranzato, Francesco

PY - 1995

Y1 - 1995

N2 - The reduced product of abstract domains is a rather well known operation in abstract interpretation. In this paper we study the inverse operation, which we call complementation. Such an operation allows to systematically decompose domains; it provides a systematic way to design new abstract domains; it allows to simplify domain verification problems, like correctness proofs; and it yields space saving representations for domains. We show that the complement exists in most cases, and we apply complementation to two well known abstract domains, notably to the Cousot and Cousot's comportment domain for analysis of functional languages and to the complex domain Sharing for aliasing analysis of logic languages.

AB - The reduced product of abstract domains is a rather well known operation in abstract interpretation. In this paper we study the inverse operation, which we call complementation. Such an operation allows to systematically decompose domains; it provides a systematic way to design new abstract domains; it allows to simplify domain verification problems, like correctness proofs; and it yields space saving representations for domains. We show that the complement exists in most cases, and we apply complementation to two well known abstract domains, notably to the Cousot and Cousot's comportment domain for analysis of functional languages and to the complex domain Sharing for aliasing analysis of logic languages.

UR - https://www.scopus.com/pages/publications/84955569216

UR - https://www.scopus.com/pages/publications/84955569216#tab=citedBy

U2 - 10.1007/3-540-60360-3_35

DO - 10.1007/3-540-60360-3_35

M3 - Conference contribution

AN - SCOPUS:84955569216

SN - 9783540603603

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 100

EP - 117

BT - Static Analysis - 2nd International Symposium, SAS 1995, Proceedings

A2 - Mycroft, Alan

PB - Springer-Verlag

T2 - 2nd International Static Analysis Symposium, SAS 1995

Y2 - 25 September 1995 through 27 September 1995

ER -

Complementation in abstract interpretation

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this