Compositional Optimization of Disjunctive Abstract Interpretations
By: R. Giacobazzi and F. Ranzato
Dip. di Informatica
Univ. di Pisa
Corso Italia 40, 56125 Pisa (Italy)
We define the inverse operation for
disjunctive completion of abstract interpretations,
introducing the notion of least disjunctive basis
for an abstract domain D: this is the most abstract domain inducing
the same disjunctive completion as D.
We show that the least disjunctive basis
exists in most cases,
and study its properties in relation with reduced
product of abstract interpretations.
The resulting framework is powerful enough to be applied to arbitrary
abstract domains for analysis, providing advanced
algebraic methods for domain manipulation and optimization.
These notions are applied
to domains for analysis of functional and logic programming languages.