Détection des fonctions de rang linéaires à terme

Abstract : Program termination is a hot research topic in program analysis. The last a 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 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 polynomial algorithm.
Complete list of metadatas

http://hal.univ-reunion.fr/hal-01187205
Contributor : Nicolas Alarcon <>
Submitted on : Friday, November 23, 2018 - 6:59:48 AM
Last modification on : Thursday, March 28, 2019 - 11:24:11 AM

File

jfpc13.pdf
Explicit agreement for this submission

Identifiers

  • HAL Id : hal-01187205, version 1

Citation

Anthony Alezan, Roberto Bagnara, Frédéric Mesnard, Etienne Payet. Détection des fonctions de rang linéaires à terme. Journées Francophones de Programmation par Contraintes (JFPC 2013), Jun 2013, Aix-en-Provence, France. ⟨hal-01187205⟩

Share

Metrics

Record views

122

Files downloads

5