Complementation of abstract domains made easy

In standard abstract interpretation theory, the inverse of the reduced product of abstract domains was recently defined and called complementation. Given two domains C and D such that D abstracts C , the complement C ∼ D is the most abstract domain whose reduced product with D gives C back. We show that, when C is a continuous complete lattice, there is a particularly simple method for computing C ∼ D . Since most domains for abstract interpretation are (complete and) continuous, this method is widely applicable. In order to demonstrate its relevance, we apply this result and some of its consequences to Cousot and Cousot’s domain for integer interval analysis of imperative programs, and to several well- known domains for the static analysis of logic languages, viz., Pos, Def and Sharing. In particular, we decompose Sharing in three more abstract domains whose reduced product gives back Sharing, and such that each component corresponds to one of the three properties that coexist in the elements of Sharing: ground-dependency, pair-sharing (or equivalently variable independence) and set-sharing. Using our theory, we minimize each component of this decomposition obtaining in some case domains that are surprisingly simpler than the corresponding original components.