DROPS

Artifact

Software

CoqInterval

Authors: Paul Geneau de Lamarlière and Guillaume Melquiond

Abstract

Cite as

Paul Geneau de Lamarlière, Guillaume Melquiond. CoqInterval (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22454,
   title = {{CoqInterval}}, 
   author = {Geneau de Lamarli\`{e}re, Paul and Melquiond, Guillaume},
   note = {Software, version 4.10.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:78da3e6e98b7ef018180119255ce1e10a048cc88;origin=https://gitlab.inria.fr/coqinterval/interval.git;visit=swh:1:snp:c1aa8c7d68f6002ef304d4d2ea6f5170da9efb39}{\texttt{swh:1:dir:78da3e6e98b7ef018180119255ce1e10a048cc88}} (visited on 2024-11-28)},
   url = {https://gitlab.inria.fr/coqinterval/interval.git},
   doi = {10.4230/artifacts.22454},
}

Document

DOI: 10.4230/LIPIcs.ITP.2024.14

End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation

Authors: Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

Designing an efficient yet accurate floating-point approximation of a mathematical function is an intricate and error-prone process. This warrants the use of formal methods, especially formal proof, to achieve some degree of confidence in the implementation. Unfortunately, the lack of automation or its poor interplay with the more manual parts of the proof makes it way too costly in practice. This article revisits the issue by proposing a methodology and some dedicated automation, and applies them to the use case of a faithful binary64 approximation of exponential. The peculiarity of this use case is that the target of the formal verification is not a simple modeling of an external code; it is an actual floating-point function defined in the logic of the Coq proof assistant, which is thus usable inside proofs once its correctness has been fully verified. This function presents all the attributes of a state-of-the-art implementation: bit-level manipulations, large tables of constants, obscure floating-point transformations, exceptional values, etc. This function has been integrated into the proof strategies of the CoqInterval library, bringing a 20× speedup with respect to the previous implementation.

Cite as

Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond. End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{faissole_et_al:LIPIcs.ITP.2024.14,
  author =	{Faissole, Florian and Geneau de Lamarli\`{e}re, Paul and Melquiond, Guillaume},
  title =	{{End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.14},
  URN =		{urn:nbn:de:0030-drops-207420},
  doi =		{10.4230/LIPIcs.ITP.2024.14},
  annote =	{Keywords: Program verification, floating-point arithmetic, formal proof, automated reasoning, mathematical library}
}

Search Results

Documents authored by Geneau de Lamarlière, Paul

CoqInterval

Abstract

Cite as

End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation

Abstract

Cite as

Thanks for your feedback!

Could not send message