Transformation de Programmes pour des Nombres Réels Fiables

This thesis presents an algorithm that eliminates square root and division operations in some straight-line programs used in embedded systems while preserving the semantics. Eliminating these two operations allows to avoid errors at runtime due to rounding. These errors can lead to a completely unexpected behavior from the program. This transformation respects the constraints of embedded systems, such as the need for the program to be executed in a fixed size memory. The transformation uses two fundamental algorithms developed in this thesis. The first one allows to eliminate square roots and divisions from Boolean expressions built with comparisons of arithmetic expressions. The second one is an algorithm that solves a particular anti-unification problem, that we call constrained anti-unification. This program transformation is defined and proven in the PVS proof assistant. It is also implemented as a strategy for this system. Con- strained anti-unification is also used to extend this transformation to programs containing functions. It allows to eliminate square roots and divisions from PVS specifications. Robustness of this method is highlighted by a major example: the elimination of square roots and divisions in a conflict detection algorithm used in aeronautics.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