Skip to Main content Skip to Navigation
Conference papers

Formal Verification of a State-of-the-Art Integer Square Root

Guillaume Melquiond 1 Raphaël Rieu-Helft 2, 1
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
Abstract : We present the automatic formal verification of a state-of-the-art algorithm from the GMP library that computes the square root of a 64-bit integer. Although it uses only integer operations, the best way to understand the program is to view it as a fixed-point arithmetic algorithm that implements Newton's method. The C code is short but intricate, involving magic constants and intentional arithmetic overflows. We have verified the algorithm using the Why3 tool and automated solvers such as Gappa.
Complete list of metadatas

Cited literature [7 references]  Display  Hide  Download

https://hal.inria.fr/hal-02092970
Contributor : Raphaël Rieu-Helft <>
Submitted on : Monday, April 8, 2019 - 3:34:17 PM
Last modification on : Wednesday, September 16, 2020 - 5:31:19 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Guillaume Melquiond, Raphaël Rieu-Helft. Formal Verification of a State-of-the-Art Integer Square Root. ARITH-26 2019 - 26th IEEE 26th Symposium on Computer Arithmetic, Jun 2019, Kyoto, Japan. pp.183-186, ⟨10.1109/ARITH.2019.00041⟩. ⟨hal-02092970⟩

Share

Metrics

Record views

143

Files downloads

213