Home |
Personal Info |
Papers |
Teaching |
Links |
Widening Operators for Weakly-Relational Numeric Abstractions
Roberto Bagnara
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Patricia M. Hill
School of Computing
University of Leeds
Leeds, LS2 9JT
United Kingdom
Elena Mazzi
Dipartimento di Matematica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Enea Zaffanella
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 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: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.
[Page last updated on August 24, 2005, 09:13:14.]
bagnara@cs.unipr.it
Home | Personal | Papers | Teaching | Links