In standard abstract interpretation theory, the inverse of the reduced product of abstract domains was recently defined and called complementation. Given two domains C and D such that D abstracts C , the complement C ∼ D is the most abstract domain whose reduced product with D gives C back. We show that, when C is a continuous complete lattice, there is a particularly simple method for computing C ∼ D . Since most domains for abstract interpretation are (complete and) continuous, this method is widely applicable. In order to demonstrate its relevance, we apply this result and some of its consequences to Cousot and Cousot’s domain for integer interval analysis of imperative programs, and to several well- known domains for the static analysis of logic languages, viz., Pos, Def and Sharing. In particular, we decompose Sharing in three more abstract domains whose reduced product gives back Sharing, and such that each component corresponds to one of the three properties that coexist in the elements of Sharing: ground-dependency, pair-sharing (or equivalently variable independence) and set-sharing. Using our theory, we minimize each component of this decomposition obtaining in some case domains that are surprisingly simpler than the corresponding original components.

Complementation of abstract domains made easy

FILE', GILBERTO;RANZATO, FRANCESCO
1996

Abstract

In standard abstract interpretation theory, the inverse of the reduced product of abstract domains was recently defined and called complementation. Given two domains C and D such that D abstracts C , the complement C ∼ D is the most abstract domain whose reduced product with D gives C back. We show that, when C is a continuous complete lattice, there is a particularly simple method for computing C ∼ D . Since most domains for abstract interpretation are (complete and) continuous, this method is widely applicable. In order to demonstrate its relevance, we apply this result and some of its consequences to Cousot and Cousot’s domain for integer interval analysis of imperative programs, and to several well- known domains for the static analysis of logic languages, viz., Pos, Def and Sharing. In particular, we decompose Sharing in three more abstract domains whose reduced product gives back Sharing, and such that each component corresponds to one of the three properties that coexist in the elements of Sharing: ground-dependency, pair-sharing (or equivalently variable independence) and set-sharing. Using our theory, we minimize each component of this decomposition obtaining in some case domains that are surprisingly simpler than the corresponding original components.
Logic Programing, Proceedings of the 1996 Joint International Conference and Syposium on Logic Programming, Bonn, Germany
0262631733
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

Caricamento 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: http://hdl.handle.net/11577/182285
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact