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.

Complementation in abstract interpretation

FILE', GILBERTO;RANZATO, FRANCESCO
1995

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.
1995
Static Analysis, Second International Symposium, SAS'95, Glasgow, UK
2nd International Static Analysis Symposium, SAS 1995
9783540603603
File in questo prodotto:
File Dimensione Formato  
sas95.pdf

accesso aperto

Tipologia: Preprint (submitted version)
Licenza: Accesso libero
Dimensione 173.75 kB
Formato Adobe PDF
173.75 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/182286
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? ND
  • OpenAlex ND
social impact