[PPL-devel] [GIT] ppl/w3ppl(master): Added BagnaraMPZ10TR.

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Wed Apr  7 21:28:33 2010 +0200

Added BagnaraMPZ10TR.

---

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

diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib
index ee137a7..fe8ae8c 100644
--- a/htdocs/Documentation/ppl.bib
+++ b/htdocs/Documentation/ppl.bib
@@ -373,6 +373,40 @@
               algorithm for the domain of \emph{octagonal shapes}.",
 }
 
+ at Techreport{BagnaraMPZ10TR,
+  Author = "R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella",
+  Title = "The Automatic Synthesis of Linear Ranking Functions:
+           The Complete Unabridged Version",
+  Number = 498,
+  Type = "Quaderno",
+  Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy",
+  Year = 2010,
+  Note = "Available at \url{http://www.cs.unipr.it/Publications/}.
+          Also published as {\tt arXiv:cs.PL/1004.0944},
+          available from \url{http://arxiv.org/}.",
+  Abstract = "The classical technique for proving termination of a
+              generic sequential computer program involves the
+              synthesis of a \emph{ranking function} for each loop of
+              the program.  \emph{Linear} ranking functions are
+              particularly interesting because many terminating loops
+              admit one and algorithms exist to automatically
+              synthesize it.  In this paper we present two such
+              algorithms: one based on work dated 1991 by Sohn and
+              Van~Gelder; the other, due to Podelski and Rybalchenko,
+              dated 2004.  Remarkably, while the two algorithms will
+              synthesize a linear ranking function under exactly the
+              same set of conditions, the former is mostly unknown to
+              the community of termination analysis and its general
+              applicability has never been put forward before the
+              present paper.  In this paper we thoroughly justify both
+              algorithms, we prove their correctness, we compare their
+              worst-case complexity and experimentally evaluate their
+              efficiency, and we present an open-source implementation
+              of them that will make it very easy to include
+              termination-analysis capabilities in automatic program
+              verifiers."
+}
+
 @InProceedings{BagnaraRZH02,
   Author = "R. Bagnara and E. Ricci and E. Zaffanella and P. M. Hill",
   Title = "Possibly Not Closed Convex Polyhedra