Improving Abstract Interpretations by Systematic Lifting to the Powerset.
Gilberto Filé, Francesco Ranzato · Padua Research Archive (University of Padova) · 1994
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: (1) A formal definition of the powerset operator is given. For any given abstract interpretation bD= , where D is the abstract domain and o_1,...,o_k are the abstract operations, this operator provides a new abstract interpretation P(bD)= . Thus, the powerset concerns also the abstract operations o_i^*, that are constructively defined from the o_i's. (2) A necessary and sufficient condition guaranteeing that P(D) is strictly better than D is given. (3) 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.