Refining and compressing 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 Cousot and Cousot's abstract interpretation theory, we present a general framework to define, study and handle operators modifying abstract domains. In particular, we introduce the notions of operators of refinement and compression of abstract domains: A refinement enhances the precision of an abstract domain; a compression operator (compressor) can exist relatively to a given refinement, and it simplifies as much as possible a domain of input for that refinement. The adequateness of our framework is shown by the fact that most of the existing operators on abstract domains fall in it. A precise relationship of adjunction between refinements and compressors is also given, justifying why compressors can be understood as inverses of refinements.
Related papers:
  • Complementation in abstract interpretation (ACM TOPLAS 19(1):7-47, 1997)
  • A Unifying View on Abstract Domain Design (ACM Comp. Surveys 28(2), 1996)
  • Weak Relative Pseudo-Complements of Closure Operators (Alg. Univ. 36(3):405-412, 1996)
  • Complementing Logic Program Semantics (LNCS 1139, Springer-Verlag, 1996)
  • Compositional Optimization of Disjunctive Abstract Interpretations (LNCS 1058, Springer-Verlag, 1996)
  • Functional Dependencies and Moore-Set Completions of Abstract Interpretations and Semantics (ILPS'95, The MIT Press, 1995)

    • Available: DVI, PostScript, BibTeX Entry.

    giaco@sci.univr.it