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
Preprints, Working Papers, ...

WhyMP, a Formally Verified Arbitrary-Precision Integer Library

Guillaume Melquiond 1 Raphaël Rieu-Helft 2
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
Inria Saclay - Ile de France, LRI - Laboratoire de Recherche en Informatique
Abstract : Arbitrary-precision integer libraries such as GMP are a critical building block of computer algebra systems. GMP provides state-of-the-art algorithms that are intricate enough to justify formal verification. In this paper, we present a C library that has been formally verified using the Why3 verification platform in about four person-years. This verification deals not only with safety, but with full functional correctness. It has been performed using a mixture of mechanically checked handwritten proofs and automated theorem proving. We have implemented and verified a nontrivial subset of GMP's algorithms, including their optimizations and intricacies. Our library provides the same interface as GMP and is almost as efficient for smaller inputs. We detail our verification methodology and the algorithms we have implemented, and include some benchmarks to compare our library with GMP.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Contributor : Guillaume Melquiond Connect in order to contact the contributor
Submitted on : Monday, May 24, 2021 - 10:52:09 AM
Last modification on : Friday, February 4, 2022 - 3:14:06 AM
Long-term archiving on: : Wednesday, August 25, 2021 - 6:03:53 PM


Files produced by the author(s)


  • HAL Id : hal-03233220, version 1


Guillaume Melquiond, Raphaël Rieu-Helft. WhyMP, a Formally Verified Arbitrary-Precision Integer Library. 2020. ⟨hal-03233220⟩



Record views


Files downloads