Complementation in Abstract Interpretation
By: A. Cortesi, G. File', R. Giacobazzi, C. Palamidessi
and F. Ranzato
Dip. di Informatica
Univ. di Pisa
Italia 40, 56125 Pisa
Reduced product of abstract domains is a rather well-known
operation for domain composition in abstract interpretation. In
this article, we study its inverse operation, introducing a notion
of domain complementation in abstract interpretation (see here
for the corresponding result in Lattice Theory).
Complementation provides a systematic way to design new abstract
domains, and it allows to systematically decompose domains. Also,
such an operation allows to simplify domain verification problems,
and it yields space-saving representations for complex domains. We
show that the complement exists in most cases, and we apply
complementation to three well-known abstract domains, notably to
Cousot and Cousot's interval domain for integer variable analysis,
to Cousot and Cousot's domain for comportment analysis of functional
languages, and to the domain Sharing for aliasing
analysis of logic languages.
This paper is an extended version of
Complementation in Abstract Interpretation (LNCS Vol. 983, Springer-Verlag, 1995).