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.File | Dimensione | Formato | |
---|---|---|---|
c-ready.pdf
embargo fino al 31/12/2026
Tipologia:
Published (publisher's version)
Licenza:
Accesso gratuito
Dimensione
180.24 kB
Formato
Adobe PDF
|
180.24 kB | 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.