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

Author: Roberto Bagnara bagnara@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}.", }

+@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/%7D. + Also published as {\tt arXiv:cs.PL/1004.0944}, + available from \url{http://arxiv.org/%7D.", + 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