Optimal domains for disjunctive abstract interpretation
By: R. Giacobazzi and F. Ranzato
Dip. di Informatica
Univ. di Pisa
Italia 40, 56125 Pisa
In the context of standard abstract interpretation theory, we define
the inverse operation to the disjunctive completion of abstract
domains, introducing the notion of least disjunctive basis of 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, also
in relation with reduced product and complementation of abstract
domains. The resulting framework provides advanced algebraic
methodologies for abstract domain manipulation and optimization.
These notions are applied to well-known abstract domains for static
analysis of functional and logic programming languages.
This paper is an extended version of
Optimization of Disjunctive Abstract Interpretations (LNCS Vol. 1058, Springer-Verlag, 1996).