School Homepage

Papers of Patricia M. Hill

Software Support for CLP: Papers

Technical Reports at Leeds

Widening Operators for Weakly-Relational Numeric Abstractions

Roberto Bagnara
Dipartimento di Matematica
Università di Parma
Via D'Azeglio, 85/A
I-43100 Parma
Italy

Patricia M. Hill
School of Computing
The University of Leeds
Leeds LS2 9JT
England

Elena Mazzi
Dipartimento di Matematica
Università di Parma
Via D'Azeglio, 85/A
I-43100 Parma
Italy

Enea Zaffanella
Dipartimento di Matematica
Università di Parma
Via D'Azeglio, 85/A
I-43100 Parma
Italy

Abstract:

We discuss the construction of proper widening operators on several weakly-relational numeric abstractions. Our proposal differs from previous ones in that we actually consider the semantic abstract domains, whose elements are geometric shapes, instead of the (more concrete) syntactic abstract domains of constraint networks and matrices. Since the closure by entailment operator preserves geometric shapes, but not their syntactic expressions, our widenings are immune from the divergence issues that could be faced by the previous approaches when interleaving the applications of widening and closure. The new widenings, which are variations of the standard widening for convex polyhedra defined by Cousot and Halbwachs, can be made as precise as the previous proposals working on the syntactic domains. The implementation of each new widening relies on the availability of an effective reduction procedure for the considered constraint description: we provide such an algorithm for the domain of octagonal shapes.

Available: Gzipped postscript. BibTeX entry.
[Page last updated on 2005/04/14.]