Automations for verifying floating-point algorithms

Guillaume Melquiond 1, 2
2 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
Abstract : Floating-point numbers are limited both in range and in precision, yet they are widely used as a way to implement computations on real numbers. Thus arithmetic operations cause small errors that might be amplified during subsequent computations. As such, it is important to guarantee that the computed values are still close enough to the ideal results. The traditional way to tackle the verification of such programs is to perform an error analysis, possibly using automated tools. Unfortunately, when it comes to the low-level floating-point functions found in mathematical libraries, the code is usually so contrived that this approach falls short. Falling back to a pen-and-paper proof makes it possible to verify such functions, but this process is long, tedious, and error-prone. Formal proofs take care of that last point, but they come at an even greater cost for the user. Thus one needs to recover some automations inside proof assistants to ease the verification process. This talk will present an overview of some of the methods available for the Coq proof assistant. In particular, it will focus on Gappa and some other interval-based automations. The presentation will not really be about the inner workings of these methods, but rather show how they can be used in practice to verify some floating-point algorithms in Coq.
Type de document :
Communication dans un congrès
5th Coq Workshop, Jul 2013, Rennes, France
Liste complète des métadonnées
Contributeur : Guillaume Melquiond <>
Soumis le : mercredi 28 janvier 2015 - 16:14:18
Dernière modification le : vendredi 23 février 2018 - 13:42:41


  • HAL Id : hal-01110666, version 1



Guillaume Melquiond. Automations for verifying floating-point algorithms. 5th Coq Workshop, Jul 2013, Rennes, France. 〈hal-01110666〉



Consultations de la notice