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
-
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
-
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
-
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
-
- 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
-
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
-
- 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
-
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
-
- 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
-