Complementation in abstract interpretation

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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 languageEnglish
Title of host publicationStatic Analysis - 2nd International Symposium, SAS 1995, Proceedings
EditorsAlan Mycroft
PublisherSpringer Verlag
Pages100-117
Number of pages18
ISBN (Print)9783540603603
DOIs
Publication statusPublished - 1 Jan 1995
Externally publishedYes
Event2nd International Static Analysis Symposium, SAS 1995 - Glasgow, United Kingdom
Duration: 25 Sept 199527 Sept 1995

Publication series

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

Conference

Conference2nd International Static Analysis Symposium, SAS 1995
Country/TerritoryUnited Kingdom
CityGlasgow
Period25/09/9527/09/95

Fingerprint

Dive into the research topics of 'Complementation in abstract interpretation'. Together they form a unique fingerprint.

Cite this