Precise Widening Operators for Convex Polyhedra (TR)

[Page last updated on "January 21, 2013, 11:18:11".] 

Roberto Bagnara, Patricia M. Hill, Elisa Ricci, and Enea Zaffanella

Abstract

Convex polyhedra constitute the most used abstract domain
among those capturing numerical relational information. 
Since the domain of convex polyhedra admits infinite ascending
chains, it has to be used in conjunction with appropriate
mechanisms for enforcing and accelerating convergence of the
fixpoint computation. 
Widening operators provide a simple and general characterization
for such mechanisms. 
For the domain of convex polyhedra, the original widening operator
proposed by Cousot and Halbwachs amply deserves the name of
standard widening since most analysis and verification tools
that employ convex polyhedra also employ that operator. 
Nonetheless, there is demand for more precise widening operators
that still has not been fulfilled. 
In this paper, after a formal introduction to the standard widening
where we clarify some aspects that are often overlooked, we embark
on the challenging task of improving on it. 
We present a framework for the systematic definition of new and
precise widening operators for convex polyhedra. 
The framework is then instantiated so as to obtain a new widening
operator that combines several heuristics and uses the standard widening
as a last resort so that it is never less precise. 
A preliminary experimental evaluation has yielded promising results. 
We also suggest an improvement to the well-known widening delay
technique that allows to gain precision while preserving its overall
simplicity.