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

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Sun Apr 1 12:55:00 2012 +0200

Added BagnaraMPZ12TR.

---

doc/ppl.bib | 36 +++++++++++++++++++++++++++++++++--- 1 files changed, 33 insertions(+), 3 deletions(-)

diff --git a/doc/ppl.bib b/doc/ppl.bib index 92c0700..339a567 100644 --- a/doc/ppl.bib +++ b/doc/ppl.bib @@ -379,9 +379,39 @@ 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.", + Note = "Superseded by \cite{BagnaraMPZ12TR}.", + 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." +} + +@Misc{BagnaraMPZ12TR, + Author = "R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella", + Title = "The Automatic Synthesis of Linear Ranking Functions: + The Complete Unabridged Version", + Howpublished = "Report {\tt arXiv:cs.PL/1004.0944v2}", + Year = 2012, + Note = "Available at \url{http://arxiv.org/%7D + and \url{http://bugseng.com/products/ppl/%7D. + Improved version of \cite{BagnaraMPZ10TR}.", 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