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 denition of the powerset operator is given. For any given ab-stract interpretation D = hD; o1; : : : ; oki, where D is the abstract domain and interpretation P (D) = hP (D); o?1; : : : ; o ki. Thus, the powerset concerns also the abstract operations o?i, that are constructively dened from the oi's. A necessary and sucient condition guaranteeing that P (D) is strictly better than D is given. The general theory is applied to the well-known abstract interpretationPROP for ground-dependence analysis of logic programs. It is shown that P (PROP) is strictly better than PROP.