We introduce the operation of domain compression for complete refinements of finite abstract domains. This provides a systematic method for simplifying abstract domains in order to isolate the most abstract domain, when it exists, whose refinement toward completeness for a given semantic function returns a given domain. Domain compression is particularly relevant to compare abstractions in static program analysis and abstract model checking. In this latter case we consider domain compression in predicate abstraction of transition systems.
Domain Compression for Complete Abstractions
GIACOBAZZI, Roberto;MASTROENI, Isabella
2003-01-01
Abstract
We introduce the operation of domain compression for complete refinements of finite abstract domains. This provides a systematic method for simplifying abstract domains in order to isolate the most abstract domain, when it exists, whose refinement toward completeness for a given semantic function returns a given domain. Domain compression is particularly relevant to compare abstractions in static program analysis and abstract model checking. In this latter case we consider domain compression in predicate abstraction of transition systems.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
C4-vmcai03.pdf
solo utenti autorizzati
Tipologia:
Versione dell'editore
Licenza:
Accesso ristretto
Dimensione
787.72 kB
Formato
Adobe PDF
|
787.72 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.