A Unifying View of Abstract Domain Design

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