A static analysis by abstract interpretation is typically composed of an ascending phase followed by a descending one. The descending phase is used to improve the precision of the analysis after that a post-fixpoint has been reached. Termination is often guaranteed by using narrowing operators, especially on numerical domains which are generally endowed with infinite descending chains. Under the hypothesis of dealing with reducible flow graphs, we provide an abstract semantics which improves the analysis precision and we show that, for a large class of numerical abstract domains over integer variables (such as intervals, octagons, template parallelotopes and template polyhedra), infinite descending chains cannot arise and we can safely omit narrowing. The abstract semantics is a slight variation of the standard one and can be easily implemented. We also provide an acceleration procedure which ensures termination of the descending phase without narrowing even with non-reducible graphs. Finally, we propose a new family of weak narrowing operators for real variables which improve the analysis precision. © 2017, Springer-Verlag Berlin Heidelberg.

Descending chains and narrowing on template abstract domains

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

Abstract

A static analysis by abstract interpretation is typically composed of an ascending phase followed by a descending one. The descending phase is used to improve the precision of the analysis after that a post-fixpoint has been reached. Termination is often guaranteed by using narrowing operators, especially on numerical domains which are generally endowed with infinite descending chains. Under the hypothesis of dealing with reducible flow graphs, we provide an abstract semantics which improves the analysis precision and we show that, for a large class of numerical abstract domains over integer variables (such as intervals, octagons, template parallelotopes and template polyhedra), infinite descending chains cannot arise and we can safely omit narrowing. The abstract semantics is a slight variation of the standard one and can be easily implemented. We also provide an acceleration procedure which ensures termination of the descending phase without narrowing even with non-reducible graphs. Finally, we propose a new family of weak narrowing operators for real variables which improve the analysis precision. © 2017, Springer-Verlag Berlin Heidelberg.
File in questo prodotto:
File Dimensione Formato  
actainf16.pdf

accesso aperto

Tipologia: Documento in Post-print
Dimensione 294.22 kB
Formato Adobe PDF
294.22 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/668972
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact