Some Formal Tools for Computer Arithmetic: Flocq and Gappa - Laboratoire Méthodes Formelles Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

Some Formal Tools for Computer Arithmetic: Flocq and Gappa

Résumé

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

Dates et versions

hal-03233227 , version 1 (24-05-2021)

Identifiants

  • HAL Id : hal-03233227 , version 1

Citer

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⟩
140 Consultations
403 Téléchargements

Partager

Gmail Facebook X LinkedIn More