Sites Inria

English version

Publication

29/11/2017

Arithmétique informatique et preuves formelles

L'ouvrage "Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System" , co-écrit par Sylvie Boldo et Guillaume Melquiond, tous deux chercheurs au sein de l'équipe de recherche Toccata du centre Inria Saclay - Île-de-France, vient de paraître aux éditions Iste.

Résumé :

L'arithmétique à virgule flottante constitue une brique essentielle du calcul moderne car c'est l'approche privilégiée pour approcher les nombres réels. Son amplitude et sa précision étant limitées, son utilisation peut vite devenir complexe et entraîner de nombreuses défaillances. Pour grandement accroître la confiance dans un logiciel numérique, une possibilité est de vérifier formellement sa preuve de correction.

Ce livre détaille le processus formel, à l'aide de l'assistant de preuve Coq, pour spécifier et vérifier des algorithmes numériques subtils. Il décrit Flocq, une formalisation de l'arithmétique à virgule flottante, ainsi que des méthodes pour automatiser les démonstrations. Il présente ensuite la spécification et la vérification d'algorithmes variés allant des EFT (transformations sans erreur) à un schéma numérique d'une équation aux dérivées partielles. Les exemples considèrent non seulement les algorithmes mathématiques mais aussi les programmes C ainsi que la problématique de la compilation.

Mots-clés : Sylvie Boldo Guillaume Melquiond Inria Saclay - Île-de-France Toccata Calcul formel

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !