@Article{BagnaraHZ09FMSD,
  Author = "R. Bagnara and P. M. Hill and E. Zaffanella",
  Title = "Weakly-Relational Shapes for Numeric Abstractions: Improved
           Algorithms and Proofs of Correctness",
  Journal = "Formal Methods in System Design",
  Volume = 35,
  Number = 3,
  Publisher = "Springer-Verlag, Berlin",
  Year = 2009,
  Pages = "279--323",
  Abstract = "Weakly-relational numeric constraints provide a
              compromise between complexity and expressivity that is
              adequate for several applications in the field of formal
              analysis and verification of software and hardware systems.
              We address the problems to be solved for the construction
              of full-fledged, efficient and provably correct abstract
              domains based on such constraints. We first propose to work
              with \emph{semantic} abstract domains, whose elements are
              \emph{geometric shapes}, instead of the (more concrete)
              syntactic abstract domains of constraint networks and
              matrices on which the previous proposals are based.
              This allows to solve, once and for all, the problem whereby
              \emph{closure by entailment}, a crucial operation for the
              realization of such domains, seemed to impede the
              realization of proper widening operators. In our approach,
              the implementation of widenings relies on the availability
              of an effective reduction procedure for the considered
              constraint description: one for the domain of \emph{bounded
              difference shapes} already exists in the literature; we
              provide algorithms for the significantly more complex cases
              of rational and integer \emph{octagonal shapes}.
              We also improve upon the state-of-the-art by presenting,
              along with their proof of correctness, closure by entailment
              algorithms of reduced complexity for domains based on
              rational and integer octagonal constraints.
              The consequences of implementing weakly-relational numerical
              domains with floating point numbers are also discussed.",
}