Un Coq apprend à un bébé Colibri à flotter
Résumé
L'arithmétique flottante est connue pour être un sujet difficile. Ses propriétés contreintuitives rendent l'écriture d'algorithmes manipulant les nombres flottants propice à de nombreuses erreurs. Des outils automatiques pour la vérification de programmes flottants existent mais ces outils faisant eux-mêmes usage de calculs en arithmétique flottante, on peut se poser la question de leur propre fiabilité. Dans cet article, nous proposons de vérifier formellement l'implémentation de raisonnements sur les nombres flottants dans le solveur de contraintes Colibri2. En particulier, nous présentons une méthodologie pour mener la preuve de correction de propagateurs de contraintes en utilisant l'assistant de preuve Coq. Nous discutons également de l'intégration des raisonnements prouvés à un développement logiciel complet en OCaml.
Domaines
Informatique [cs]
Origine : Fichiers produits par l'(les) auteur(s)