@Article{BagnaraHZ06STTT,
  Author = "R. Bagnara and P. M. Hill and E. Zaffanella",
  Title = "Widening Operators for Powerset Domains",
  Journal = "Software Tools for Technology Transfer",
  Publisher = "Springer-Verlag, Berlin",
  Volume = 8,
  Number = "4/5",
  Pages = "449--466",
  Year = 2006,
  Note = "As the figures in the journal version of this paper have
          been improperly printed (rendering them useless), we
          recommend that interested readers download an electronic
          copy from this web site or contact one of the authors for a
          printed copy.",
  Abstract = "The \emph{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.",
  URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ06STTT.pdf"
}