Roberto, Margherita and Beatrice

Home

Personal Info

Papers

Teaching

Links

Widening Operators for Powerset Domains (TR)

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

Enea Zaffanella
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 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 three generic widening operators for the finite powerset abstract domain. The 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: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.

[Page last updated on January 22, 2004, 21:21:00.]

© Roberto Bagnara
bagnara@cs.unipr.it

Home | Personal | Papers | Teaching | Links