Improving abstract interpretations by systematic lifting to the powerset

Operators that systematically produce more precise abstract interpretations from simpler ones are interesting. In this paper we present a formal study of one such operator: the powerset. The main achievements of the paper are described below: • A formal definition of the powerset operator is given. For any given abstract interpretation D = ⟨D, o1, . . . , ok⟩, where D is the abstract domain and o1, . . . , ok are the abstract operations, this operator provides a new abstract interpretation P(D) = ⟨P(D),o⋆1,...,o⋆k⟩. Thus, the powerset concerns also the abstract operations o⋆i , that are constructively defined from the oi’s. • A necessary and sufficient condition guaranteeing that P (D) is strictly better than D is given. • The general theory is applied to the well-known abstract interpretation PROP for ground-dependence analysis of logic programs. It is shown that P(PROP) is strictly better than PROP.