Complementation in abstract interpretation

Abstract. The reduced product of abstract domains is a rather well known operation in abstract interpretation. In this paper we study the inverse op-eration, which we call complementation. Such an operation allows to sys-tematically decompose domains; it provides a systematic way to design new abstract domains; it allows to simplify domain verication problems, like cor-rectness proofs; and it yields space saving representations for domains. We show that the complement exists in most cases, and we apply complementa-tion 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.