Home |
Personal Info |
Papers |
Teaching |
Links |
Eventual Linear Ranking Functions
Roberto Bagnara
BUGSENG and Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Fred Mesnard
LIM/IREMIA
Université de La Réeunion
Parc Technologique Universitaire
2, rue Joseph Wetzell - Bât 2
F-97490 Sainte Clotilde
La Réunion
France
Abstract:
Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for programming languages such as C and Java with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of declarative constraint programming. In this paper, we first recall an algorithm based on Farkas' Lemma for discovering linear ranking functions proving termination of a certain class of loops. Then we propose an extension of this method for showing the existence of eventual linear ranking functions, i.e., linear functions that become ranking functions after a finite unrolling of the loop. We show correctness and completeness of this algorithm.
Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.
[Page last updated on July 18, 2013, 22:15:22.]
bagnara@cs.unipr.it
Home | Personal | Papers | Teaching | Links