< Retour au sommaire

Soutenance de thèse de Maxime Jacquemin

Titre: Arithmétiques relationnelles pour l'analyse par interprétation abstraite de propriétés de précision numérique

le

Lieu: https://app.livestorm.co/cea_list/soutenance-de-these-maxime-jacquemin?type=light

Résumé

L’arithmétique à virgule flottante est l’approche la plus utilisée pour réaliser des calculs mathématiques reposant sur les nombres réels avec un ordinateur. Cependant, elle souffre d’un défaut: chaque opération peut introduire une erreur, c’est-à-dire une différence avec le résultat que nous aurions obtenu en utilisant des réels. Bien que ces erreurs soient très faibles, elles peuvent s’accumuler et provoquer des bugs ayant parfois des conséquences graves, en particulier dans des domaines critiques comme l’aéronautique ou le nucléaire. Il est donc nécessaire de pouvoir garantir que les erreurs introduites par l’utilisation de l’arithmétique flottante ne causent pas de problème, ou, dit autrement, qu’elles soient suffisamment faibles pour que le programme se comporte comme attendu. Pour répondre à ce besoin, nous proposons une analyse statique par interprétation abstraite, reposant sur un nouveau domaine abstrait, et calculant une sur-approximation des erreurs introduites par l’arithmétique flottante. Cette analyse repose sur l’interaction, au travers d’un produit réduit, entre deux conceptions de la notion d’erreur: l’erreur absolue, intuitive et permettant de mieux comprendre le programme analysé, et l’erreur relative, plus proche du fonctionnement de l’arithmétique flottante. Notre analyse repose sur la combinaison des arithmétiques affines et d’intervalles, et dispose de capacités de raisonnements relationnels. Cette combinaison a cependant des difficultés à traiter les opérations non linéaires, dont la précision impacte fortement l’évaluation des erreurs relatives. Nous proposons donc deux approches pour répondre à ce problème. La première consiste en différentes améliorations de cette combinaison, permettant d’évaluer plus précisément multiplications et divisions sans impacter significativement les performances. La seconde consiste en la définition d’une nouvelle arithmétique relationnelle, spécifiquement conçue pour représenter l’erreur relative. Par ailleurs, nous avons implémenté un prototype de notre analyse au sein de l’outil Frama-C/Eva. Les premiers résultats expérimentaux montrent l’intérêt de notre analyse par rapport à l’état de l’art.

Jury