Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Journal articles

A Why3 proof of GMP algorithms

Raphaël Rieu-Helft 1, 2 
2 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
Abstract : Large-integer arithmetic algorithms are used in contexts where both their performance and their correctness are critical, such as cryptographic software. The fastest algorithms are complex enough that formally verifying them is desirable but challenging. We have formally verified a comprehensive arbitrary-precision integer arithmetic library that implements many state-of-the-art algorithms from the GMP library. The algorithms we have verified include addition, subtraction, Toom-Cook multiplication, division and square root. We use the Why3 platform to perform the proof semi-automatically. We obtain an efficient and formally verified C library of low-level functions on arbitrary-precision natural integers. This verification covers the functional correctness of the algorithms, as well as the memory safety and absence of arithmetic overflows of their C implementation. Using detailed pseudocode, we present the algorithms that we verified and outline their proofs.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Raphaël Rieu-Helft Connect in order to contact the contributor
Submitted on : Thursday, February 13, 2020 - 2:45:44 PM
Last modification on : Saturday, June 25, 2022 - 10:44:28 PM
Long-term archiving on: : Thursday, May 14, 2020 - 3:20:16 PM


Files produced by the author(s)



Raphaël Rieu-Helft. A Why3 proof of GMP algorithms. Journal of Formalized Reasoning, ASDD-AlmaDL, 2019, ⟨10.6092/issn.1972-5787/9730⟩. ⟨hal-02477578⟩



Record views


Files downloads