Formally verified certificate checkers for hardest-to-round computation

Érik Martin-Dorel 1, * Guillaume Hanrot 2 Micaela Mayero 3 Laurent Théry 4
* Auteur correspondant
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
2 ARIC - Arithmetic and Computing
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
4 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In order to derive efficient and robust floating-point implementations of a given function f, it is crucial to compute its hardest-to-round points, i.e. the floating-point numbers x such that f(x) is closest to the midpoint of two consecutive floating-point numbers. Depending on the floating-point format one is aiming at, this can be highly computationally intensive. In this paper, we show how certificates based on Hensel's lemma can be added to an algorithm using lattice basis reduction so that the result of a computation can be formally checked in the Coq proof assistant.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (1), pp.1-29. <10.1007/s10817-014-9312-2>
Liste complète des métadonnées


https://hal.inria.fr/hal-00919498
Contributeur : Érik Martin-Dorel <>
Soumis le : vendredi 19 décembre 2014 - 17:28:22
Dernière modification le : vendredi 17 février 2017 - 16:10:21
Document(s) archivé(s) le : samedi 15 avril 2017 - 11:20:17

Fichier

Hensel-JAR.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, Laurent Théry. Formally verified certificate checkers for hardest-to-round computation. Journal of Automated Reasoning, Springer Verlag, 2015, 54 (1), pp.1-29. <10.1007/s10817-014-9312-2>. <hal-00919498v2>

Partager

Métriques

Consultations de
la notice

477

Téléchargements du document

51