Publications HAL

2023

Journal articles

titre
WhyMP, a Formally Verified Arbitrary-Precision Integer Library
auteur
Guillaume Melquiond, Raphaël Rieu-Helft
article
Journal of Symbolic Computation, 2023, 115, pp.74-95. ⟨10.1016/j.jsc.2022.07.007⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03233220/file/main.pdf BibTex

2020

Conference papers

titre
WhyMP, a Formally Verified Arbitrary-Precision Integer Library
auteur
Guillaume Melquiond, Raphaël Rieu-Helft
article
ISSAC 2020 - 45th International Symposium on Symbolic and Algebraic Computation, Jul 2020, Kalamata, Greece. pp.352-359, ⟨10.1145/3373207.3404029⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02566654/file/main.pdf BibTex

2019

Journal articles

titre
A Why3 proof of GMP algorithms
auteur
Raphaël Rieu-Helft
article
Journal of Formalized Reasoning, 2019, ⟨10.6092/issn.1972-5787/9730⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02477578/file/main.pdf BibTex

Conference papers

titre
Formal Verification of a State-of-the-Art Integer Square Root
auteur
Guillaume Melquiond, Raphaël Rieu-Helft
article
ARITH-26 2019 - 26th IEEE 26th Symposium on Computer Arithmetic, Jun 2019, Kyoto, Japan. pp.183-186, ⟨10.1109/ARITH.2019.00041⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02092970/file/main.pdf BibTex
titre
Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP
auteur
Raphaël Rieu-Helft
article
JFLA 2019 - 30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Rousses, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01943010/file/main.pdf BibTex

2018

Conference papers

titre
A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms
auteur
Guillaume Melquiond, Raphaël Rieu-Helft
article
9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.178-193, ⟨10.1007/978-3-319-94205-6_13⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01699754/file/main.pdf BibTex
titre
Un mécanisme d'extraction vers C pour Why3
auteur
Raphaël Rieu-Helft
article
29èmes Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01653153/file/main.pdf BibTex

2017

Conference papers

titre
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library
auteur
Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond
article
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⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01519732/file/main.pdf BibTex
titre
Result graphs for an abstract interpretation-based static analyzer
auteur
Pascal Cuoq, Raphaël Rieu-Helft
article
28èmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
Accès au texte intégral et bibtex
https://hal.science/hal-01503064/file/main.pdf BibTex