Optimal domains for disjunctive abstract interpretation

By: R. Giacobazzi and F. Ranzato

Roberto Giacobazzi
Dip. di Informatica
Univ. di Pisa
Corso Italia 40, 56125 Pisa (Italy)
giaco@di.unipi.it

Abstract:

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).