Arithmétique des Ordinateurs et Preuves Formelles

Guillaume Melquiond 1
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Cet exposé s'intéresse aux liens entre arithmétique des ordinateurs et vérification automatique, que ce soit pour de la preuve de programmes ou de théorèmes, le tout dans le cadre formel de l'assistant de preuve Coq. L'exposé est construit en deux parties. La première s'intéresse à la preuve automatique de théorèmes mathématiques à l'aide de méthodes venues de l'arithmétique des ordinateurs. Il s'agit d'abord d'implanter et de formaliser une arithmétique à virgule flottante simplifiée mais efficace afin d'approcher les calculs réels. Puis une arithmétique d'intervalles peut être implantée au-dessus, offrant un moyen fiable de calculer des bornes sur des expressions à valeurs réelles. L'arithmétique d'intervalles dans sa version naïve est certes fiable mais rarement efficace à cause de l'effet de corrélation. L'étape suivante est donc de construire des approximations polynomiales fiables pour réduire cet effet. En combinant tout cela avec de la preuve par réflexion, il est alors possible de prouver automatiquement des bornes fines sur des expressions à valeurs réelles. Le procédé peut être poussé jusqu'à des intégrales propres voire même impropres. Tout cela a été intégré à la bibliothèque CoqInterval. La deuxième partie s'intéresse à la vérification formelle d'algorithmes qui mettent en oeuvre de l'arithmétique à virgule flottante. C'était déjà le cas de certains des algorithmes de la première partie, mais l'utilisation de l'arithmétique d'intervalles les rendait en grande partie corrects par construction. Par contre, si l'on s'intéresse à des bibliothèques efficaces d'approximation de fonctions mathématiques (les « libm »), il n'y a plus rien de cela. Sans une vérification formelle, il est alors difficile de se convaincre que le code ne contient pas de nombreux bogues subtils dus à l'arithmétique à virgule flottante. Il est alors nécessaire d'effectuer une analyse fine des erreurs d'arrondi commises afin de s'assurer que les valeurs calculées par le code approchent correctement la fonction mathématique souhaitée. Mais une telle analyse est longue et difficile, surtout dans un cadre formel. C'est pour cela que l'outil Gappa a été conçu. Il permet de vérifier automatiquement des propriétés sur des algorithmes flottants, par une combinaison d'arithmétique d'intervalles, de réécriture et d'analyse de l'erreur directe. Il est aussi capable de générer des preuves formelles pour décharger des buts Coq.
Type de document :
Communication dans un congrès
Nicolas Magaud. 30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France. 2019, 〈https://dpt-info.u-strasbg.fr/~magaud/JFLA2019/〉
Liste complète des métadonnées

https://hal.inria.fr/hal-02013540
Contributeur : Guillaume Melquiond <>
Soumis le : lundi 11 février 2019 - 10:07:22
Dernière modification le : mercredi 13 février 2019 - 01:16:51

Identifiants

  • HAL Id : hal-02013540, version 1

Citation

Guillaume Melquiond. Arithmétique des Ordinateurs et Preuves Formelles. Nicolas Magaud. 30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France. 2019, 〈https://dpt-info.u-strasbg.fr/~magaud/JFLA2019/〉. 〈hal-02013540〉

Partager

Métriques

Consultations de la notice

26

Téléchargements de fichiers

21