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.
Titolo: | Domain Compression for Complete Abstractions |
Autori: | |
Data di pubblicazione: | 2003 |
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. |
Handle: | http://hdl.handle.net/11562/19662 |
ISBN: | 9783540003489 |
Appare nelle tipologie: | 04.01 Contributo in atti di convegno |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
C4-vmcai03.pdf | Versione dell'editore | Accesso ristretto | Utenti riconosciuti Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.