Module: ppl/w3ppl Branch: master Commit: e3bef523bc4b9767c4dbd5b2bd9afc86c85c9a2c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=e3bef523bc4... Author: Patricia Hill <p.m.hill@leeds.ac.uk> Date: Tue Aug 3 21:24:40 2010 +0100 Updated with paper on linear ranking functions and that the sttp paper is now published. Note that the source file address for the paper on linear ranking functions is fictitious and either this should be revised or a pdf version of the paper added at that address. (http://www.cs.unipr.it/ppl/Documentation/BagnaraMPZ10TR) --- htdocs/Documentation/papers.raw | 43 +++++++++++++++++++++++++++++++++++++- 1 files changed, 41 insertions(+), 2 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index c4444be..44aa2f3 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -122,8 +122,9 @@ supported by the PPL, is fully described. <TD> R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. - <EM>Software Tools for Technology Transfer</EM>, 2005. - To appear.<BR> + <EM>Software Tools for Technology Transfer</EM>, + 8(4-5):449-466, 2006.<BR> +[ <A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ06STTT.pdf">.pdf</A> ] <BLOCKQUOTE> Read this paper if you are interested in using powersets to express @@ -174,6 +175,44 @@ efficiency) the domains of intervals and convex polyhedra. </TR> </TABLE> +<H3>On Linear Ranking Functions</H3> +<TABLE> + +<TR valign="top"> +<TD align="right"> +[<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> +<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. + +</BLOCKQUOTE> +</TD> +</TR> +</TABLE> + <HR> <A NAME="historical">