How to Get an Efficient yet Verified Arbitrary-Precision Integer Library

Abstract : The GNU Multi-Precision library is a widely used, safety-critical, library for arbitrary-precision arithmetic. Its source code is written in C and assembly, and includes intricate state-of-the-art algorithms for the sake of high performance. Formally verifying the functional behavior of such highly optimized code, not designed with verification in mind, is challenging. We present a fully verified library designed using the Why3 program verifier. The use of a dedicated memory model makes it possible to have the Why3 code be very similar to the original GMP code. This library is extracted to C and is compatible and performance-competitive with GMP.
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01519732
Contributor : Guillaume Melquiond <>
Submitted on : Thursday, August 31, 2017 - 9:40:30 AM
Last modification on : Monday, December 9, 2019 - 5:24:07 PM
Long-term archiving on: Friday, December 1, 2017 - 5:56:08 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond. How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. pp.84-101, ⟨10.1007/978-3-319-72308-2_6⟩. ⟨hal-01519732v2⟩

Share

Metrics

Record views

522

Files downloads

1575