[PPL-devel] [GIT] ppl/w3ppl(master): Added bibtex entry for BagnaraHZ09 ( submitted for publication).

[Enea Zaffanella]

Module: ppl/w3ppl
Branch: master
Commit: 62da5b310035206635d82a0a0e688af5a525f4c1
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=62da5b310035206635d82a0a0e688af5a525f4c1

Author: Enea Zaffanella <zaffanella at cs.unipr.it>
Date:   Tue Apr  7 15:54:08 2009 +0200

Added bibtex entry for BagnaraHZ09 (submitted for publication).

---

 htdocs/Documentation/ppl.bib |   35 +++++++++++++++++++++++++++++++++++
 1 files changed, 35 insertions(+), 0 deletions(-)

diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib
index 56b4e40..2784df5 100644
--- a/htdocs/Documentation/ppl.bib
+++ b/htdocs/Documentation/ppl.bib
@@ -896,6 +896,41 @@
   URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TCS.pdf"
 }
 
+ at Unpublished{BagnaraHZ09,
+  Author = "R. Bagnara and P. M. Hill and E. Zaffanella",
+  Title = "Weakly-Relational Shapes for Numeric Abstractions: Improved
+           Algorithms and Proofs of Correctness",
+  Year = 2009,
+  Note = "Submitted for publication",
+  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.",
+}
+
 @InProceedings{BalasundaramK89,
   Author = "V. Balasundaram and K. Kennedy",
   Title = "A Technique for Summarizing Data Access