In the context of the standard Cousot and Cousot framework, refinement operators that systematically produce more precise abstract interpretations from simpler ones are useful. We present a theoretical study of one such operator: the powerset. For any given abstract interpretation, i.e. an abstract domain equipped with corresponding abstract operations, the powerset operator yields a new abstract interpretation, where the abstract domain is (very close to) the powerset of the original one and the operations are accordingly extended. It turns out that the refined powerset domain is able to represent in the best possible way the concrete disjunction. Conditions that guarantee the correctness of the powerset operator are given, and the relationship, with respect to the precision, between any abstract interpretation and its powerset is studied. The general theory is applied to the well-known abstract interpretation POS, typically used for ground-dependency analysis of logic languages. We show that the powerset P(POS) is strictly more precise than POS both at the domain and operations level. Furthermore, the standard bottom-up abstract semantics of logic programs based on POS and P(POS) are compared by exhibiting a completeness relationship between them, i.e. the first semantics can be obtained by abstracting back the second one.

The powerset operator on abstract interpretations

RANZATO, FRANCESCO
1999

Abstract

In the context of the standard Cousot and Cousot framework, refinement operators that systematically produce more precise abstract interpretations from simpler ones are useful. We present a theoretical study of one such operator: the powerset. For any given abstract interpretation, i.e. an abstract domain equipped with corresponding abstract operations, the powerset operator yields a new abstract interpretation, where the abstract domain is (very close to) the powerset of the original one and the operations are accordingly extended. It turns out that the refined powerset domain is able to represent in the best possible way the concrete disjunction. Conditions that guarantee the correctness of the powerset operator are given, and the relationship, with respect to the precision, between any abstract interpretation and its powerset is studied. The general theory is applied to the well-known abstract interpretation POS, typically used for ground-dependency analysis of logic languages. We show that the powerset P(POS) is strictly more precise than POS both at the domain and operations level. Furthermore, the standard bottom-up abstract semantics of logic programs based on POS and P(POS) are compared by exhibiting a completeness relationship between them, i.e. the first semantics can be obtained by abstracting back the second one.
File in questo prodotto:
File Dimensione Formato  
publishedPaper.pdf

embargo fino al 31/12/2029

Tipologia: Published (Publisher's Version of Record)
Licenza: Accesso gratuito
Dimensione 1.96 MB
Formato Adobe PDF
1.96 MB Adobe PDF Visualizza/Apri   Richiedi una copia
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/2961099
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 28
  • ???jsp.display-item.citation.isi??? 19
  • OpenAlex ND
social impact