Completeness in abstract interpretation: a domain perspective

Completeness in abstract interpretation is an ideal and rare situation where the abstract semantics is able to take full advantage of the power of representation of the underlying abstract domain. In this paper, we develop an algebraic theory of completeness in abstract interpretation. We show that completeness is an abstract domain property and we prove that there always exist both the greatest complete restriction and the least complete extension of any abstract domain, with respect to continuous semantic functions. Under certain hypotheses, a constructive procedure for computing these complete domains is given. These methodologies provide advanced algebraic tools for manipulating abstract interpretations, which can be fruitfully used both in program analysis and in semantics design.