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.
2003
9783540003489
Abstract interpretation; abstract domains; completeness; domain refinement; predicate abstraction; abstract model-checking; program analysis
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/19662
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 4
social impact