On the Linear Ranking Problem for Simple Floating-Point Loops

Abstract : Termination of loops can be inferred from the existence of linear ranking functions. We already know that the existence of thesefunctions is PTIME decidable for simple rational loops. Since very recently, we know that the problem is coNP-complete for simple integer loops. We continue along this path by investigating programs dealing with floating-point computations. First, we show that the problem is at least in coNP for simple floating-point loops. Then, in order to work around that theoretical limitation we present an algorithm which remains polynomial by sacrificing completeness. The algorithm, based on the Podelski-Rybalchenko algorithm, can also synthesize in polynomial time the linear ranking functions it detects. To our knowledge, our work is the first adaptation of this well-known algorithm to floating-points.
Type de document :
Communication dans un congrès
Xavier Rival. 23rd International Symposium on Static Analysis (SAS), Sep 2016, Edinburgh, United Kingdom. Springer, Lecture Notes in Computer Science, Proceedings of the 23rd International Symposium on Static Analysis (SAS), 9837, pp.300-316, 2016, 〈10.1007/978-3-662-53413-7_15〉
Liste complète des métadonnées

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

http://hal.univ-reunion.fr/hal-01451688
Contributeur : Réunion Univ <>
Soumis le : lundi 5 novembre 2018 - 11:04:45
Dernière modification le : jeudi 8 novembre 2018 - 01:18:04

Fichier

sas16.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Etienne Payet, Fonenantsoa Maurica, Frédéric Mesnard. On the Linear Ranking Problem for Simple Floating-Point Loops. Xavier Rival. 23rd International Symposium on Static Analysis (SAS), Sep 2016, Edinburgh, United Kingdom. Springer, Lecture Notes in Computer Science, Proceedings of the 23rd International Symposium on Static Analysis (SAS), 9837, pp.300-316, 2016, 〈10.1007/978-3-662-53413-7_15〉. 〈hal-01451688〉

Partager

Métriques

Consultations de la notice

20

Téléchargements de fichiers

2