Skip to Main content Skip to Navigation
Conference papers

WhyMP, a Formally Verified Arbitrary-Precision Integer Library

Guillaume Melquiond 1 Raphaël Rieu-Helft 2, 1
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.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-02566654
Contributor : Guillaume Melquiond <>
Submitted on : Saturday, August 8, 2020 - 3:58:55 PM
Last modification on : Friday, July 2, 2021 - 11:20:43 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Guillaume Melquiond, Raphaël Rieu-Helft. WhyMP, a Formally Verified Arbitrary-Precision Integer Library. ISSAC 2020 - 45th International Symposium on Symbolic and Algebraic Computation, Jul 2020, Kalamata, Greece. pp.352-359, ⟨10.1145/3373207.3404029⟩. ⟨hal-02566654v2⟩

Share

Metrics

Record views

108

Files downloads

706