Compositional optimization of disjunctive abstract interpretations

Abstract. We dene the inverse operation for disjunctive completion, in-troducing 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 domains for analysis, providing advanced algebraic methods for domain ma-nipulation and optimization. These notions are applied to abstract domains for analysis of functional and logic programming languages.