Widening Operators for Powerset Domains

Publication TypeJournal Article
Year of Publication2006
AuthorsBagnara R, Hill PM, Zaffanella E
JournalSoftware Tools for Technology Transfer
Keywordsabstract interpretation, convex polyhedra, disjunctive refinement, finite powerset construction, powersets, software verification, static analysis, widening

The finite powerset construction upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. While most of the operations on the finite powerset abstract domain are easily obtained by ‘‘lifting’’ the corresponding operations on the base-level domain, the problem of endowing finite powersets with a provably correct widening operator is still open. In this paper we define three generic widening methodologies 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 that allow all the flexibility required to tune the complexity/precision trade-off. As far as we know, this is the first time that the problem of deriving non-trivial, provably correct widening operators in a domain refinement is tackled successfully. We illustrate the proposed techniques by instantiating our widening methodologies on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known.

File attachments: 
We are a passionate team of experts. Do not hesitate to let us have your feedback:
You may be surprised to discover just how much your suggestions matter to us.