[PPL-devel] [GIT] ppl/ppl(master): Added BagnaraMPZ12TR.
Roberto Bagnara
bagnara at cs.unipr.it
Sun Apr 1 12:55:11 CEST 2012
Module: ppl/ppl
Branch: master
Commit: cecfd8d5f80648656ad87d47b48be0119cb0d686
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cecfd8d5f80648656ad87d47b48be0119cb0d686
Author: Roberto Bagnara <bagnara at 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/}.
- Also published as {\tt arXiv:cs.PL/1004.0944},
- available from \url{http://arxiv.org/}.",
+ 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."
+}
+
+ at 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/}
+ and \url{http://bugseng.com/products/ppl/}.
+ 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
More information about the PPL-devel
mailing list