Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Doctorat de

Doctorat
Equipe : Toccata

Eviter les guet-apens des compilateurs : preuves formelles de programmes avec nombres flottants.

Début le 01/02/2009
Direction : MARCHÉ, Claude
[Sylvie BOLDO]

Ecole doctorale :
Etablissement d'inscription : Université Paris-Sud

Lieu de déroulement : INRIA Saclay

Soutenue le 11/06/2012 devant le jury composé de :
Sylvie BOLDO
Florent HIVERT
Xavier LEROY
Claude MARCHÉ
David MONNIAUX (rapporteur)
Jean-Michel MULLER
César MUNOZ (rapporteur)

Activités de recherche :

Résumé :
Sur des architectures récentes, un programme numérique peut donner des réponses différentes en fonction du hardware et du compilateur. Ces incohérences des résultats viennent du fait que chaque calcul en virgule flottante est effectué avec des précisions différentes.
Le but de cette thèse est de prouver formellement des propriétés des programmes opérant sur des nombres flottants en prenant en compte l’architecture et le compilateur. Pour le faire, nous avons proposé deux approches différentes. La première approche est de prouver des propriétés des programmes en virgule flottante qui sont vraies sur plusieurs architectures et compilateurs. Cette approche ne considère que les erreurs d’arrondi qui doivent être validées quels que soient l’environnement matériel et le choix du compilateur. Elle est implantée dans la plate-forme Frama-C pour l’analyse statique de code C. La deuxième approche consiste à prouver des propriétés des programmes en analysant leur code assembleur. Nous nous concentrons sur des problèmes et des pièges qui apparaissent sur des calculs en virgule flottante. L’analyse directe du code assembleur nous permet de considérer des caratéristiques dépendant de l’architecture ou du compilateur telle que l’utilisation des registres en précision étendue. Cette approche est implantée comme une sur-couche de la plate-forme Why pour la vérification déductive.