School Homepage

Papers of Patricia M. Hill

Software Support for CLP: Papers

Technical Reports at Leeds

Widening Operators for Powerset Domains

[Page last updated on 2003/12/19.]

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

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

Abstract:

The finite powerset construction upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. In this paper we define two generic widening operators for the finite powerset abstract domain. Both widenings are obtained by lifting any widening operator defined on the base-level abstract domain and are parametric with respect to the specification of a few additional operators. We illustrate the proposed techniques by instantiating our widenings on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known.

Available: Gzipped postscript. BibTeX entry.