[PPL-devel] [GIT] ppl/w3ppl(master): Redone the part on the synthesis of linear ranking functions.

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Wed Aug  4 14:49:52 2010 +0200

Redone the part on the synthesis of linear ranking functions.
Only cite published papers.  Do not just replicate the abstract.

---

 htdocs/Documentation/papers.raw |   34 +++++++++++++---------------------
 1 files changed, 13 insertions(+), 21 deletions(-)

diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw
index 5a98265..bf72d12 100644
--- a/htdocs/Documentation/papers.raw
+++ b/htdocs/Documentation/papers.raw
@@ -198,7 +198,7 @@ and software systems (including the analysis of imperative programs).
 </TR>
 </TABLE>
 
-<H3>On Linear Ranking Functions</H3>
+<H3>On the Synthesis of Linear Ranking Functions</H3>
 <TABLE>
 
 <TR valign="top">
@@ -206,28 +206,20 @@ and software systems (including the analysis of imperative programs).
 [<A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraMPZ10TR"></A>]
 </TD>
 <TD>
-R. Bagnara, F. Mesnard, F. Pescetti, and E. Zaffanella.
-  The Automatic Synthesis of Linear Ranking Functions.
-  Submitted for publication, 2010.<BR>
+R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella.
+ The automatic synthesis of linear ranking functions: The complete
+  unabridged version.
+ Quaderno 498, Dipartimento di Matematica, Università di Parma,
+  Italy, 2010.
+ Available at <A HREF="http://www.cs.unipr.it/Publications/">http://www.cs.unipr.it/Publications/</A>.
+ Also published as <TT>arXiv:cs.PL/1004.0944</TT>, available from
+  <A HREF="http://arxiv.org/">http://arxiv.org/</A>.
 <BLOCKQUOTE>
 Read this paper if you are interested in synthesizing ranking
-functions for termination analysis.  The classical technique for
-proving termination of a generic sequential computer program involves
-the synthesis of a <EM>ranking function</EM> for each loop of the
-program.  <EM>Linear</EM> 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.
+functions for termination analysis.  The two methods presented in this
+paper are fully implemented in the PPL and make it very easy to
+include termination-analysis capabilities in automatic program
+verifiers.
 </BLOCKQUOTE>
 </TD>
 </TR>