@Inproceedings{AlezanBMP13JFPC, Author = "A. Alezan and R. Bagnara and F. Mesnard and \'E. Payet", Title = "D\'etection des fonctions de rang lin\'eaires \`a terme", Booktitle = "Actes des Neuvièmes Journées Francophones de Programmation par Contraintes (JFPC 2013)", Address = "Aix-en-Provence, France", Year = 2013, Pages = "11--20", Note = "In French", Resume = "La terminaison des programmes est un sujet actif de recherche en informatique. Ces derni\`eres ann\'ees ont vu l'apparition d'analyseurs de terminaison performants pour des langages comme C ou Java o\`u l'emploi des techniques et outils de la programmation par contraintes est omnipr\'esent. Dans cet article, nous rappelons un algorithme particulier bas\'e sur l'emploi du lemme de Farkas pour le calcul de fonctions de rang lin\'eaires garantissant la terminaison d'une certaine classe de boucles. Puis nous pr\'esentons une extension de cette m\'ethode pour la d\'ecouverte de fonctions lin\'eaires qui deviennent des fonctions de rang lin\'eaire \`a terme, c.-\`a-d.\ apr\`es un certain nombre de passages dans la boucle. Nous montrons la correction et la compl\'etude d'un algorithme polynomial pour ce probl\`eme.", 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 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 \emph{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." }