Formal Verification of a Floating-Point Expansion Renormalization Algorithm

Abstract : Many numerical problems require a higher computing precision than the one offered by standard floating-point formats. A common way of extending the precision is to use floating-point expansions. As the problems may be critical and as the algorithms used have very complex proofs (many sub-cases), a formal guarantee of correctness is a wish that can now be fulfilled, using interactive theorem proving. In this article we give a formal proof in Coq for one of the algorithms used as a basic brick when computing with floating-point expansions, the renormaliza-tion, which is usually applied after each operation. It is a critical step needed to ensure that the resulted expansion has the same property as the input one, and is more " compressed ". The formal proof uncovered several gaps in the pen-and-paper proof and gives the algorithm a very high level of guarantee.
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01512417
Contributor : Valentina Popescu <>
Submitted on : Sunday, April 23, 2017 - 12:52:53 AM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Monday, July 24, 2017 - 12:17:01 PM

File

itp17.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01512417, version 1

Citation

Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu. Formal Verification of a Floating-Point Expansion Renormalization Algorithm. 8th International Conference on Interactive Theorem Proving (ITP'2017), Sep 2017, Brasilia, Brazil. ⟨hal-01512417⟩

Share

Metrics

Record views

1046

Files downloads

624