Linear refinement is a technique for systematically constructing more precise abstract domains for program analysis starting from the basic domain which represents just the property of interest. We use here linear refinement to construct a domain for pair-independence and freeness analysis of logic programs which is strictly more precise than Jacobs and Langen's domain for sharing analysis endowed with freeness information. Moreover, it can be used for abstract compilation, while Jacobs and Langen's domain can only be used for abstract interpretation. We provide an approximate representation of our domain and algorithms for the abstract operations. We describe an implementation of an analyser which uses abstract compilation over our domain and its evaluation over a set of benchmarks. This shows that its precision is comparable to that of a traditional sharing and freeness analysis performed through abstract interpretation. To the best of our knowledge, this is the first implementation of a sharing analysis based on abstract compilation, as well as the first implementation of a static analysis based on a new domain developed through linear refinement.

Pair-Independence and Freeness Analysis through Linear Refinement

SPOTO, Nicola Fausto
2003

Abstract

Linear refinement is a technique for systematically constructing more precise abstract domains for program analysis starting from the basic domain which represents just the property of interest. We use here linear refinement to construct a domain for pair-independence and freeness analysis of logic programs which is strictly more precise than Jacobs and Langen's domain for sharing analysis endowed with freeness information. Moreover, it can be used for abstract compilation, while Jacobs and Langen's domain can only be used for abstract interpretation. We provide an approximate representation of our domain and algorithms for the abstract operations. We describe an implementation of an analyser which uses abstract compilation over our domain and its evaluation over a set of benchmarks. This shows that its precision is comparable to that of a traditional sharing and freeness analysis performed through abstract interpretation. To the best of our knowledge, this is the first implementation of a sharing analysis based on abstract compilation, as well as the first implementation of a static analysis based on a new domain developed through linear refinement.
static analysis; abstract interpretation; sharing; freeness; linear refinement
File in questo prodotto:
File Dimensione Formato  
PairIndependence.pdf

solo utenti autorizzati

Tipologia: Versione dell'editore
Licenza: Accesso ristretto
Dimensione 415.34 kB
Formato Adobe PDF
415.34 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: http://hdl.handle.net/11562/16662
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 4
social impact