Widening Operators for Powerset Domains

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 powerset abstract domain. The widenings are obtained by lifting ning 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.

• Type: Conference
• Year: 2004
• Where: VMCAI
• Authors: Roberto Bagnara, Patricia M. Hill, Enea Zaffanella
• Keywords: Abstract Domain, Powerset Abstract Domain, Software Engineering, VMCAI 2004, Widening Operator