A Quest for Exactness: Program Transformation for Reliable Real Numbers

Résumé : Cette thèse présente un algorithme qui élimine les racines carrées et les divisions dans des programmes sans boucles, utilisés dans des systèmes embarqués, tout en préservant la sémantique. L'élimination de ces opérations permet d'éviter les erreurs d'arrondis à l'exécution, ces erreurs d'arrondis pouvant entraîner un comportement complètement inattendu de la part du programme. Cette trans- formation respecte les contraintes du code embarqué, en particulier la nécessité pour le programme produit de s'exécuter en mémoire fixe. Cette transformation utilise deux algorithmes fondamentaux développés dans cette thèse. Le premier permet d'éliminer les racines carrées et les divisions des expressions booléennes contenant des comparaisons d'expressions arithmétiques. Le second est un algorithme qui résout un problème d'anti-unification particulier, que nous appelons anti-unification contrainte. Cette transformation de programme est définie et prouvée dans l'assistant de preuves PVS. Elle est aussi implantée comme une stratégie de ce système. L'anti-unification contrainte est aussi utilisée pour étendre la transformation à des programmes contenant des fonctions. Elle permet ainsi d'éliminer les racines carrées et les divisions de spécifications écrites en PVS. La robustesse de cette méthode est mise en valeur par un exemple conséquent: l'élimination des racines carrées et des divisions dans un programme de détection des conflits aériens.
Type de document :
Thèse
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English
Liste complète des métadonnées

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

https://pastel.archives-ouvertes.fr/pastel-00960808
Contributeur : Pierre Néron <>
Soumis le : mardi 18 mars 2014 - 17:04:02
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : jeudi 19 juin 2014 - 14:43:55

Fichier

Identifiants

  • HAL Id : pastel-00960808, version 1

Collections

Citation

Pierre Neron. A Quest for Exactness: Program Transformation for Reliable Real Numbers. Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English. 〈pastel-00960808〉

Partager

Métriques

Consultations de la notice

372

Téléchargements de fichiers

251