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

Résumé : La terminaison des programmes est un sujet actif de recherche en informatique. Ces dernières années ont vu l'apparition d'analyseurs de terminaison performants pour des langages comme C ou Java où l'emploi des techniques et outils de la programmation par contraintes est omniprésent. Dans cet article, nous rappelons un algorithme particulier basé sur l'emploi du lemme de Far-kas pour le calcul de fonctions de rang linéaires garantissant la terminaison d'une certaine classe de boucles. Puis nous présentons une extension de cette méthode pour la découverte de fonctions linéaires qui deviennent des fonctions de rang linéaire à terme, c'est-à-dire après un certain nombre de passages dans la boucle. Nous montrons la correction et la complétude d'un algorithme polynomial pour ce problème.
Type de document :
Communication dans un congrès
Truchet, Charlotte. Journées Francophones de Programmation par Contraintes (JFPC 2013), Jun 2013, Aix-en-Provence, France. 2013
Liste complète des métadonnées

http://hal.univ-reunion.fr/hal-01187205
Contributeur : Nicolas Alarcon <>
Soumis le : vendredi 23 novembre 2018 - 06:59:48
Dernière modification le : samedi 24 novembre 2018 - 01:25:16

Fichier

jfpc13.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-01187205, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

99

Téléchargements de fichiers

1