In the theory of abstract interpretation, a descending phase may be used to improve the precision of the analysis after a post-fixpoint has been reached. Termination is often guaranteed by using narrowing operators. This is especially true on numerical domains, since they are generally endowed with infinite descending chains which may lead to a non-terminating descending phase in the absence of narrowing. We provide an abstract semantics which improves the analysis precision and shows that, for a large class of numerical abstract domains over integer variables (such as intervals, octagons and template polyhedra), it is possible to avoid infinite descending chains and omit narrowing. Moreover, we propose a new family of narrowing operators for real variables which improves the analysis precision.

Narrowing Operators on Template Abstract Domains

AMATO, Gianluca
;
DI NARDO DI MAIO, SIMONE;MEO, MARIA CHIARA;SCOZZARI, Francesca
2015-01-01

Abstract

In the theory of abstract interpretation, a descending phase may be used to improve the precision of the analysis after a post-fixpoint has been reached. Termination is often guaranteed by using narrowing operators. This is especially true on numerical domains, since they are generally endowed with infinite descending chains which may lead to a non-terminating descending phase in the absence of narrowing. We provide an abstract semantics which improves the analysis precision and shows that, for a large class of numerical abstract domains over integer variables (such as intervals, octagons and template polyhedra), it is possible to avoid infinite descending chains and omit narrowing. Moreover, we propose a new family of narrowing operators for real variables which improves the analysis precision.
Lecture Notes in Computer Science
978-331919248-2
File in questo prodotto:
File Dimensione Formato  
fm15.pdf

accesso aperto

Descrizione: Conference Paper
Tipologia: Documento in Post-print
Dimensione 322.01 kB
Formato Adobe PDF
322.01 kB Adobe PDF Visualizza/Apri

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/11564/644414
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact