and

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. 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 comportmen