In the context of Cousot and Cousot's abstract interpretation theory, we present a general framework to define, study and handle operators modifying abstract domains. In particular, we introduce the notions of operators of refinement and compression of abstract domains: A refinement enhances the precision of an abstract domain; a compression operator (compressor) can exist relatively to a given refinement, and it simplifies as much as possible a domain of input for that refinement. 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 refinements and compressors is also given, justifying why compressors can be understood as inverses of refinements.
Refining and compressing abstract domains
RANZATO, FRANCESCO
1997
Abstract
In the context of Cousot and Cousot's abstract interpretation theory, we present a general framework to define, study and handle operators modifying abstract domains. In particular, we introduce the notions of operators of refinement and compression of abstract domains: A refinement enhances the precision of an abstract domain; a compression operator (compressor) can exist relatively to a given refinement, and it simplifies as much as possible a domain of input for that refinement. 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 refinements and compressors is also given, justifying why compressors can be understood as inverses of refinements.File | Dimensione | Formato | |
---|---|---|---|
published-paper-springer.pdf
accesso aperto
Tipologia:
Published (publisher's version)
Licenza:
Accesso gratuito
Dimensione
1.74 MB
Formato
Adobe PDF
|
1.74 MB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.