We abstract a denotational trace semantics for an imperative language into a compositional and focussed watchpoint semantics. Every abstraction of its computational domain induces an abstract, still compositional and focussed watchpoint semantics. We describe its implementation and instantiation with a domain of signs. It shows that its space and time costs are proportional to the number of watchpoints and that abstract compilation reduces those costs significantly.

Watchpoint Semantics: A Tool for Compositional and Focussed Static Analyses

SPOTO, Nicola Fausto
2001

Abstract

We abstract a denotational trace semantics for an imperative language into a compositional and focussed watchpoint semantics. Every abstraction of its computational domain induces an abstract, still compositional and focussed watchpoint semantics. We describe its implementation and instantiation with a domain of signs. It shows that its space and time costs are proportional to the number of watchpoints and that abstract compilation reduces those costs significantly.
static analysis; denotational semantics; abstract interpretation
File in questo prodotto:
File Dimensione Formato  
Watchpoint-semantics.pdf

solo utenti autorizzati

Tipologia: Versione dell'editore
Licenza: Accesso ristretto
Dimensione 344.13 kB
Formato Adobe PDF
344.13 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/16670
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 2
social impact