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

Raphaël Rieu-Helft 1, 2, 3 Claude Marché 2, 3 Guillaume Melquiond 2, 3
3 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Type de document :
Communication dans un congrès
Andrei Paskevich; Thomas Wies. 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. 10712, pp.84-101, 2017, Lecture Notes in Computer Science. 〈https://vstte17.lri.fr/〉. 〈10.1007/978-3-319-72308-2_6〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01519732
Contributeur : Guillaume Melquiond <>
Soumis le : jeudi 31 août 2017 - 09:40:30
Dernière modification le : jeudi 11 janvier 2018 - 06:25:27
Document(s) archivé(s) le : vendredi 1 décembre 2017 - 17:56:08

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond. How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. Andrei Paskevich; Thomas Wies. 9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. 10712, pp.84-101, 2017, Lecture Notes in Computer Science. 〈https://vstte17.lri.fr/〉. 〈10.1007/978-3-319-72308-2_6〉. 〈hal-01519732v2〉

Partager

Métriques

Consultations de la notice

102

Téléchargements de fichiers

54