Completeness in abstract interpretation: A domain perspective

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:

Completeness in abstract interpretation is an ideal and rare situation where, for a given abstract domain A, no additional loss of precision is introduced by approximating the meaning of programs by evaluating their semantics in A. Therefore, complete abstract domains can be rightfully considered as optimal. In this paper we develop a general theory of completeness for abstract domains and, in this context, we show that there always exist both the least complete extension and the greatest complete restriction (called complete kernel) of any abstract domain wrt any family of continuous semantic operations. Also, under certain hypotheses, an algorithm computing such a least complete extension for an abstract domain is given. These methodologies provide advanced algebraic tools for manipulating and comparing domains which can be used both in the field of abstract interpretation-based program analysis and in semantics design. A number of examples illustrating these techniques are given in the field of integer variable and logic program analysis.