Formally verified certificate checkers for hardest-to-round computation

Érik Martin-Dorel 1, * Guillaume Hanrot 2 Micaela Mayero 3 Laurent Théry 4
* Corresponding author
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
Inria Saclay - Ile de France, LRI - Laboratoire de Recherche en Informatique
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.
Complete list of metadatas

Cited literature [32 references]  Display  Hide  Download

https://hal.inria.fr/hal-00919498
Contributor : Érik Martin-Dorel <>
Submitted on : Friday, December 19, 2014 - 5:28:22 PM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Saturday, April 15, 2017 - 11:20:17 AM

File

Hensel-JAR.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

792

Files downloads

326