[PPL-devel] [GIT] ppl/ppl(master): Added BagnaraMPZ12IC.
Roberto Bagnara
bagnara at cs.unipr.it
Sun Apr 1 13:01:35 CEST 2012
Module: ppl/ppl
Branch: master
Commit: 4ca090268809487aae781880548a6805c198d1f0
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4ca090268809487aae781880548a6805c198d1f0
Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date: Sun Apr 1 13:01:26 2012 +0200
Added BagnaraMPZ12IC.
---
doc/ppl.bib | 30 ++++++++++++++++++++++++++++++
1 files changed, 30 insertions(+), 0 deletions(-)
diff --git a/doc/ppl.bib b/doc/ppl.bib
index 339a567..57f5f49 100644
--- a/doc/ppl.bib
+++ b/doc/ppl.bib
@@ -435,6 +435,36 @@
verifiers."
}
+ at Article{BagnaraMPZ12IC,
+ Author = "R. Bagnara and F. Mesnard and A. Pescetti and E. Zaffanella",
+ Title = "A New Look at the Automatic Synthesis of Linear Ranking Functions",
+ Journal = "Information and Computation",
+ Publisher = "Elsevier Science B.V.",
+ Year = 2012,
+ Note = "To appear."
+ 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
More information about the PPL-devel
mailing list