Complementation in Abstract Interpretation
By: A. Cortesi, G. File', R. Giacobazzi, C. Palamidessi and F. Ranzato
Dip. di Informatica
Univ. di Pisa
Corso Italia 40, 56125 Pisa (Italy)
The reduced product of abstract domains is a rather
well known operation in abstract interpretation.
In this paper we study the inverse operation,
which we call complementation.
Such an operation allows to systematically decompose
domains; it provides a systematic way
to design new abstract domains; it allows to simplify
problems, like correctness proofs; and it yields space saving
representations for domains.
We show that the complement
exists in most cases, and we apply complementation to two well known
abstract domains, notably to the
Cousot and Cousot's comportment domain for analysis of functional
languages and to the complex domain
Sharing for aliasing analysis of logic languages.
See here for the journal version.