HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Some Formal Tools for Computer Arithmetic: Flocq and Gappa

Sylvie Boldo 1 Guillaume Melquiond 1
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
Abstract : This invited paper presents two tools developed by the authors. Their purpose is to help the user in writing proofs regarding computer arithmetic, e.g., certifying a bound on a round-off error, while aiming at a high level of guarantee. Flocq is a library of mathematical definitions and theorems for the Coq proof assistant; Gappa is meant to compute bounds of values and errors, while producing the corresponding formal proof. We describe here these tools, how they interact and how they fit in a larger verification process.
Complete list of metadata

Contributor : Guillaume Melquiond Connect in order to contact the contributor
Submitted on : Monday, May 24, 2021 - 10:59:16 AM
Last modification on : Wednesday, February 9, 2022 - 5:26:06 PM
Long-term archiving on: : Wednesday, August 25, 2021 - 6:04:15 PM


Files produced by the author(s)


  • HAL Id : hal-03233227, version 1


Sylvie Boldo, Guillaume Melquiond. Some Formal Tools for Computer Arithmetic: Flocq and Gappa. ARITH 2021 - 28th IEEE International Symposium on Computer Arithmetic, Jun 2021, Online, Italy. ⟨hal-03233227⟩



Record views


Files downloads