Re ning and Compressing Abstract Domains

Abstract. In the context of Cousot and Cousot's abstract interpreta-tion theory, we present a general framework to dene, study and handle operators modifying abstract domains. In particular, we introduce the notions of operators of renement and compression of abstract domains: A renement enhances the precision of an abstract domain; a compres-sion operator (compressor) can exist relatively to a given renement, and it simplies as much as possible a domain of input for that renement. The adequateness of our framework is shown by the fact that most of the existing operators on abstract domains fall in it. A precise relationship of adjunction between renements and compressors is also given, justifying why compressors can be understood as inverses of renements.