Eventual linear ranking functions

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.
Type de document :
Communication dans un congrès
Ricardo Pena. 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, Sep 2013, Madrid, Spain. ACM Press, Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, pp.229--238, 2013, 〈10.1145/2505879.2505884〉
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

http://hal.univ-reunion.fr/hal-01451694
Contributeur : Réunion Univ <>
Soumis le : vendredi 16 novembre 2018 - 09:45:56
Dernière modification le : samedi 24 novembre 2018 - 01:25:16

Fichier

Eventual_linear_ranking_functi...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Roberto Bagnara, Frédéric Mesnard. Eventual linear ranking functions. Ricardo Pena. 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, Sep 2013, Madrid, Spain. ACM Press, Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, pp.229--238, 2013, 〈10.1145/2505879.2505884〉. 〈hal-01451694〉

Partager

Métriques

Consultations de la notice

60

Téléchargements de fichiers

2