A Unifying View on Abstract Domain Design
By: G. File', R. Giacobazzi, and F. Ranzato
Roberto
Giacobazzi
Dip. di Informatica
Univ. di Pisa
Corso
Italia 40, 56125 Pisa
(Italy)
giaco@di.unipi.it
Abstract:
The concept of abstract interpretation has been
introduced by Patrick and Radhia Cousot in 1977, in order to formalize
static program analyses. Within this framework, our goal is to offer a
unifying view on operators for enhancing and simplifying abstract
domains. Enhancing and simplifying operators are viewed,
respectively, as domain refinements and inverses of domain
refinements. This new unifying viewpoint makes both the understanding
and the design of operators on abstract domains much simpler.
Enhancing operators increase the expressiveness of an abstract domain:
they comprise the Cousot and Cousot reduced product, disjunctive
completion and reduced cardinal power, the Nielson tensor product, the
open product and the pattern completion by Cortesi et al., and the
functional dependencies by Giacobazzi and Ranzato (see here).
Simplifying operators are used to reduce complex abstract domains into
simpler ones with respect to the efficiency of the corresponding
analysis as well as with respect to the proof of their
correctness. Simplifying operators comprise the complementation of
Cortesi et al. (see here)
and the Giacobazzi and Ranzato least disjunctive basis (see here).
Available:
DVI,
PostScript,
BibTeX Entry.
giaco@sci.univr.it