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.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.