La vérification de programmes avec des calculs sur les nombres à virgule flottante est une étape très importante dans le développement de logiciels critiques. Les calculs sur les nombres flottants sont généralement imprécis, et peuvent dans certains cas diverger par rapport au résultat attendu sur les nombres réels. L’objectif de cette thèse est de concevoir un solveur de contraintes sur les nombres à virgule flottante dédié à la vérification de programmes. Nous présentons dans ce manuscrit une nouvelle méthode de résolution de contraintes sur les flottants. Cette méthode se base principalement sur la sur-approximation des contraintes sur les flottants par des contraintes sur les réels. Cette sur-approximation doit être conservative des solutions sur les flottants. Les contraintes obtenues sont ensuite résolues par un solveur de contraintes sur les réels. Nous avons proposé un algorithme de filtrage des domaines sur les flottants basé sur le concept de la sur-approximation qui utilise des techniques de programmation linéaire. Nous avons aussi proposé une méthode de recherche de solutions basée sur des heuristiques. Cette méthode offre aussi la possibilité de comparer le comportement des programmes par rapport à une spécification sur les réels. Ces méthodes ont été implémentées et expérimentées sur un ensemble de programmes avec du calcul sur les nombres flottants. / The verification of programs with floating-point numbers computation is an important issue in the development of critical software systems. Computations over floating-point numbers are not accurate, and the results may be very different from the expected results over real numbers. The aim of this thesis is to design a constraint solver over floating-point numbers for program verification purposes. We introduce a new method for solving constraints over floating-point numbers. This method is based on an over-approximation of floating-point constraints using constraints over real numbers. This overapproximation is safe, that’s to say it doesn’t loose any solution over the floats. The generated constraints are then solved with a constraint solver over real numbers. We propose a new filtering algorithm using linear programming techniques, which takes advantage of these over-approximations of floating-point constraints. We introduce also new search methods and heuristics to find floating-point solutions of these constraints. Using our implementation, we show on a set of counter-examples the difference of the execution of programs over the floats with the specification over real numbers.

La vérification de programmes avec des calculs sur les nombres à virgule flottante est une étape très importante dans le développement de logiciels critiques. Les calculs sur les nombres flottants sont généralement imprécis, et peuvent dans certains cas diverger par rapport au résultat attendu sur les nombres réels. L'objectif de cette thèse est de concevoir un solveur de contraintes sur les nombres à virgule flottante dédié à la vérification de programmes. Nous présentons dans ce manuscrit une nouvelle méthode de résolution de contraintes sur les flottants. Cette méthode se base principalement sur la sur-approximation des contraintes sur les flottants par des contraintes sur les réels. Cette sur-approximation doit être conservative des solutions sur les flottants. Les contraintes obtenues sont ensuite résolues par un solveur de contraintes sur les réels. Nous avons proposé un algorithme de filtrage des domaines sur les flottants basé sur le concept de la sur-approximation qui utilise des techniques de programmation linéaire. Nous avons aussi proposé une méthode de recherche de solutions basée sur des heuristiques. Cette méthode offre aussi la possibilité de comparer le comportement des programmes par rapport à une spécification sur les réels. Ces méthodes ont été implémentées et expérimentées sur un ensemble de programmes avec du calcul sur les nombres flottants.

Depuis l'apparition des premiers ordinateurs, l'arithmétique flottante a énormément évolué. La norme IEEE 754 a permis de fixer les caractéristiques de l'arithmétique des ordinateurs modernes, mais les scientifiques perdent de plus en plus vite le contrôle de la validité de leurs calculs. Malgré l'énorme travail associé à la définition des opérations, la validation des calculs ne peut toujours pas être assurée de façon certaine par l'arithmétique implantée sur les ordinateurs. Je présente dans la première partie de cette étude deux prolongements qui visent à augmenter la marge de validité des opérations : un nouveau mode d'arrondi pour les fonctions trigonométriques et un codage efficace des intervalles accessible facilement à l'utilisateur. Je présente aussi dans cette partie une étude détaillée de la fonction unit in the last place et la probabilité d'absorption ou de propagation des erreurs dans une chaîne de multiplication. Ces travaux, qui viennent s'ajouter aux travaux antérieurs d'autres équipes de recherche et aux solutions que j'ai proposées dans ma thèse de master montrent les bénéfices que l'on pourra tirer des deux extensions présentées. L'arithmétique en-ligne permet de gérer efficacement les problèmes de précision, mais les opérateurs élémentaires utilisés sont peu adaptés aux architectures modernes de 32 ou 64 bits. L'implantation efficace d'un opérateur en-ligne ne peut que passer par la description d'un circuit de bas niveau. Les prédiffusés actifs, terme français utilisé pour Field Programmable Gate Array, sont des composants spéciaux programmables au niveau des portes logiques. Ils permettent d'abaisser les coûts de production en évitant de fabriquer un prototype. Nous avons implanté grâce à ces technologies les opérateurs simples de calcul en-ligne : addition, normalisation, etc...Le Noyau Arithmétique de Calcul En-Ligne (Nacel) décrit dans ce mémoire permet d'implanter les opérations arithmétiques usuelles telles que la multiplication, la division, l'extraction de racine carrée et les fonctions élémentaires trigonométriques et hyperboliques par une approximation polynômiale. Les architectures à flots de données sont insensibles aux difficultés sur lesquelles butent les concepteurs des ordinateurs modernes : temps d'accès à la mémoire, latence de communication, occupation partielle du pipeline d'instructions. Je décris dans ce document le mode de fonctionnement d'une machine virtuelle appelée Petite Unité de Calcul En-ligne (Puce). Par une gestion adaptée des étiquettes inspirée pour le contrôle des données de celle utilisée par la Manchester Data Flow Machine, Puce reproduit le comportement complet d'une machine à flot de données. Elle comprend de plus les opérations en-ligne de calcul scientifique. Nous présentons afin de valider le modèle d'évaluation de Puce les résultats de simulations logicielles pour une ou plusieurs unités fonctionnelles.

Le sujet de cette thèse est le développement de méthodes pour la découverte automatique des propriétés des variables numériques d'un programme. Nous nous plaçons dans le cadre de l'interprétation abstraite et introduisons plusieurs nouveaux domaines numériques, dont celui des octogones, de coût et de précision intermédiaires entre les domaines non relationnels (peu précis) et relationnels (coûteux) existants. Nous présentons leur adaptation à l'analyse des nombres à virgule flottante, jusqu'à présent limitée aux domaines non relationnels. Enfin, nous présentons les méthodes génériques de linéarisation et de propagation symbolique améliorant leur précision pour un surcoût réduit. Les méthodes introduites dans cette thèse ont été intégr! ées à l'analyseur Astrée et appliquées à la preuve d'absence d'erreurs dans le logiciel embarqué critique de commande de vol des avions Airbus A340, justifiant ainsi l'intérêt de nos méthodes pour des cadres d'applications réelles.