Formally verified certificate checkers for hardest-to-round computation - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Automated Reasoning Année : 2015

Formally verified certificate checkers for hardest-to-round computation

Résumé

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.
Fichier principal
Vignette du fichier
Hensel-JAR.pdf (666.8 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00919498 , version 1 (16-12-2013)
hal-00919498 , version 2 (19-12-2014)

Identifiants

Citer

Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, Laurent Théry. Formally verified certificate checkers for hardest-to-round computation. Journal of Automated Reasoning, 2015, 54 (1), pp.1-29. ⟨10.1007/s10817-014-9312-2⟩. ⟨hal-00919498v2⟩
619 Consultations
376 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More