[PPL-devel] [GIT] ppl/w3ppl(master): Improved BagnaraHZ09TCS and BagnaraHZ09FMSD. Added BagnaraHZ09TRb.

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Mon Aug 10 14:50:11 2009 +0200

Improved BagnaraHZ09TCS and BagnaraHZ09FMSD.  Added BagnaraHZ09TRb.

---

 htdocs/Documentation/BagnaraHZ09TRb.pdf |  Bin 0 -> 346789 bytes
 htdocs/Documentation/ppl.bib            |   48 +++++++++++++++++++++++++++---
 2 files changed, 43 insertions(+), 5 deletions(-)

diff --git a/htdocs/Documentation/BagnaraHZ09TRb.pdf b/htdocs/Documentation/BagnaraHZ09TRb.pdf
new file mode 100644
index 0000000..d4c6300
Binary files /dev/null and b/htdocs/Documentation/BagnaraHZ09TRb.pdf differ
diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib
index 54a6121..27cec84 100644
--- a/htdocs/Documentation/ppl.bib
+++ b/htdocs/Documentation/ppl.bib
@@ -904,7 +904,7 @@
   Journal = "Formal Methods in System Design",
   Publisher = "Springer-Verlag, Berlin",
   Year = 2009,
-  Note = "Available online at
+  Note = "To appear in print.  Available online at
           \url{http://www.springerlink.com/content/d40842574t1r5877/}",
   Abstract = "Weakly-relational numeric constraints provide a
               compromise between complexity and expressivity that is
@@ -943,10 +943,11 @@
   Type = "Quaderno",
   Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy",
   Year = 2009,
-  Note = "Available at \url{http://www.cs.unipr.it/Publications/}.
-          An improved version (typos corrected in statement and proof
-          of Theorem~6.8) has been published as {\tt arXiv:cs.CG/0904.1783},
-          available from \url{http://arxiv.org/}.",
+  Note = "Available at \url{http://www.cs.unipr.it/Publications/}.  A
+          corrected and improved version (corrected an error in the
+          statement of condition (3) of Theorem~3.6, typos corrected
+          in statement and proof of Theorem~6.8) has been published
+          in \cite{BagnaraHZ09TRb}.",
   Abstract = "Deciding whether the union of two convex polyhedra is a
               convex polyhedron is a basic problem in polyhedral
               computation having important applications in the field
@@ -975,6 +976,43 @@
   URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TRa.pdf"
 }
 
+ at Misc{BagnaraHZ09TRb,
+  Author = "R. Bagnara and P. M. Hill and E. Zaffanella",
+  Title = "Exact Join Detection for Convex Polyhedra
+           and Other Numerical Abstractions",
+  Howpublished = "Report {\tt arXiv:cs.CG/0904.1783}",
+  Year = 2009,
+  Note = "Available at \url{http://arxiv.org/}
+          and \url{http://www.cs.unipr.it/ppl/}",
+  Abstract = "Deciding whether the union of two convex polyhedra is
+              itself a convex polyhedron is a basic problem in
+              polyhedral computations; having important applications
+              in the field of constrained control and in the
+              synthesis, analysis, verification and optimization of
+              hardware and software systems.  In such application
+              fields though, general convex polyhedra are just one
+              among many, so-called, \emph{numerical abstractions},
+              which range from restricted families of (not necessarily
+              closed) convex polyhedra to non-convex geometrical
+              objects.  We thus tackle the problem from an abstract
+              point of view: for a wide range of numerical
+              abstractions that can be modeled as bounded
+              join-semilattices ---that is, partial orders where any
+              finite set of elements has a least upper bound---, we
+              show necessary and sufficient conditions for the
+              equivalence between the lattice-theoretic join and the
+              set-theoretic union.  For the case of closed convex
+              polyhedra ---which, as far as we know, is the only one
+              already studied in the literature--- we improve upon the
+              state-of-the-art by providing a new algorithm with a
+              better worst-case complexity.  The results and
+              algorithms presented for the other numerical
+              abstractions are new to this paper.  All the algorithms
+              have been implemented, experimentally validated, and
+              made available in the Parma Polyhedra Library.",
+  URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09TRb.pdf"
+}
+
 @InProceedings{BalasundaramK89,
   Author = "V. Balasundaram and K. Kennedy",
   Title = "A Technique for Summarizing Data Access