The reduced relative power operation on abstract domains

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:

In the context of standard abstract interpretation theory, we define and study a systematic operator of reduced relative power for composing functionally abstract domains. The reduced relative power of two abstract domains D1 (the exponent) and D2 (the base) consists in a suitably defined lattice of monotone functions from D1 to D2, called dependencies, and it is a generalization of the Cousot and Cousot operator of reduced (cardinal) power. The relationship between the reduced relative power and Nielson's tensor product is also investigated. The case of autodependencies (when base and exponent are the same domain) turns out to be particularly interesting: Under certain hypotheses, the domain of autodependencies corresponds to a suitable powerset-like completion of the base abstract domain, providing a compact set-theoretic representation for autodependencies. The usefulness of the reduced relative power is shown by a number of applications to abstract domains used both for program analysis and for semantics design. Notably, we prove that the domain Def for logic program ground-dependency analysis can be characterized as autodependencies of a standard more abstract domain representing plain groundness only, and we show how to exploit reduced relative power to systematically derive compositional logic program semantics. This paper is an extended version of Functional dependencies and Moore-set completions of abstract interpretations and semantics (ILPS'95, 1995).

Available: DVI, PostScript, BibTeX Entry.


Related works by the authors:
  • A Unifying View on Abstract Domain Design (ACM Comp. Surveys 28(2):333-336, 1996)
  • Intuitionistic implication in abstract interpretation (PLILP'97, 1997)
  • Refining and compressing abstract domains (ICALP'97, 1997).

  • giaco@sci.univr.it