A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms

Guillaume Melquiond 1, 2 Raphaël Rieu-Helft 2, 3
2 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 : Earlier work showed that automatic verification of GMP's algorithms using Why3 exceeds the current capabilities of automatic solvers. To complete this verification, numerous cut indications had to be supplied by the user, slowing the project to a crawl. This paper shows how we have extended Why3 with a framework for proofs by reflection, with minimal impact on the trusted computing base. This framework makes it easy to write dedicated decision procedures that make full use of Why3's imperative features and are formally verified. We evaluate how much work could have been saved when verifying GMP's algorithms, had this framework been available. This approach opens the way to efficiently tackling the further verification of GMP's algorithms.
Type de document :
Communication dans un congrès
Didier Galmiche; Stephan Schulz; Roberto Sebastiani. 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.178-193, 2018, Lecture Notes in Computer Science. 〈http://ijcar2018.org/〉. 〈10.1007/978-3-319-94205-6_13〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01699754
Contributeur : Raphaël Rieu-Helft <>
Soumis le : jeudi 12 avril 2018 - 16:41:54
Dernière modification le : mardi 17 juillet 2018 - 12:11:06

Fichier

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

Identifiants

Citation

Guillaume Melquiond, Raphaël Rieu-Helft. A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms. Didier Galmiche; Stephan Schulz; Roberto Sebastiani. 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.178-193, 2018, Lecture Notes in Computer Science. 〈http://ijcar2018.org/〉. 〈10.1007/978-3-319-94205-6_13〉. 〈hal-01699754v2〉

Partager

Métriques

Consultations de la notice

393

Téléchargements de fichiers

101