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

Author: Roberto Bagnara bagnara@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.&nbsp;Bagnara, F.&nbsp;Mesnard, F.&nbsp;Pescetti, and E.&nbsp;Zaffanella. - The Automatic Synthesis of Linear Ranking Functions. - Submitted for publication, 2010.<BR> +R.&nbsp;Bagnara, F.&nbsp;Mesnard, A.&nbsp;Pescetti, and E.&nbsp;Zaffanella. + The automatic synthesis of linear ranking functions: The complete + unabridged version. + Quaderno 498, Dipartimento di Matematica, Universit&agrave; 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>