Module: ppl/ppl Branch: master Commit: 4ca090268809487aae781880548a6805c198d1f0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4ca0902688094...
Author: Roberto Bagnara bagnara@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." }
+@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