How to Get an Efficient yet Verified Arbitrary-Precision Integer Library - Archive ouverte HAL Access content directly
Conference Papers Year : 2017

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

(1, 2, 3) , (2, 3) , (2, 3)
1
2
3

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.
Fichier principal
Vignette du fichier
main.pdf (312.31 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01519732 , version 1 (09-05-2017)
hal-01519732 , version 2 (31-08-2017)

Identifiers

Cite

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⟩
482 View
1893 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More