Eventual Linear Ranking Functions

TL;DR

This paper introduces an extension to existing termination analysis techniques by developing algorithms for discovering eventual linear ranking functions, which prove loop termination after finite unrolling, enhancing the precision of program analysis.

Contribution

It proposes a novel algorithm for identifying eventual linear ranking functions, extending traditional methods based on Farkas' Lemma for proving loop termination.

Findings

Algorithm is correct and complete

Enables termination proofs after finite loop unrolling

Improves precision of termination analysis

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.