Wiki Agenda Contact Version française

Publications : Raphaël Rieu-Helft

Back
[12] Guillaume Melquiond and Raphaël Rieu-Helft. WhyMP, a formally verified arbitrary-precision integer library. Journal of Symbolic Computation, 115:74--95, 2023. [ bib | DOI | full text on HAL ]
[11] Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, and Raphaël Rieu-Helft. Formally verified bounds on rounding errors in concrete implementations of logarithm-sum-exponential functions. Research Report 9531, Inria, 2023. [ bib | full text on HAL ]
[10] Guillaume Melquiond and Raphaël Rieu-Helft. WhyMP, a formally verified arbitrary-precision integer library. In 45th International Symposium on Symbolic and Algebraic Computation (ISSAC), pages 352--359, 2020. [ bib | DOI | full text on HAL ]
Keywords: Integer arithmetic ; Deductive program verification ; Mathematical library
[9] Raphaël Rieu-Helft. Development and verification of arbitrary-precision integer arithmetic libraries. Thèse de doctorat, Université Paris-Saclay, 2020. [ bib | full text on HAL ]
Keywords: Static analysis ; Arbitrary-precision integer arithmetic ; Deductive verification of programs ; Proof by reflection ; Why3 ; Vérification déductive de programmes ; Arithmétique entière en précision arbitraire ; Analyse statique ; Preuve par réflexion ; Why3
[8] Guillaume Melquiond and Raphaël Rieu-Helft. Formal verification of a state-of-the-art integer square root. In Symposium on Computer Arithmetic, pages 183--186, Kyoto, Japan, June 2019. [ bib | full text on HAL ]
[7] Raphaël Rieu-Helft. Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP. In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019. [ bib | full text on HAL ]
[6] Raphaël Rieu-Helft. A Why3 proof of GMP algorithms. Journal of Formalized Reasoning, 2019. [ bib | DOI | full text on HAL ]
[5] Guillaume Melquiond and Raphaël Rieu-Helft. A Why3 framework for reflection proofs and its application to GMP's algorithms. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, 9th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science, Oxford, United Kingdom, July 2018. [ bib | full text on HAL ]
[4] Raphaël Rieu-Helft. Un mécanisme d'extraction vers C pour Why3. In Sylvie Boldo and Nicolas Magaud, editors, Vingt-neuvièmes Journées Francophones des Langages Applicatifs, Banyuls-sur-mer, France, January 2018. [ bib | full text on HAL | .pdf ]
[3] Raphaël Rieu-Helft, Claude Marché, and Guillaume Melquiond. How to get an efficient yet verified arbitrary-precision integer library. In 9th Working Conference on Verified Software: Theories, Tools, and Experiments, volume 10712 of Lecture Notes in Computer Science, pages 84--101, Heidelberg, Germany, July 2017. [ bib | DOI | full text on HAL | .pdf ]
Keywords: arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier
[2] Raphaël Rieu-Helft and Pascal Cuoq. Result graphs for an abstract interpretation-based static analyzer. In Sylvie Boldo and Julien Signoles, editors, Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib ]
[1] Raphaël Rieu-Helft and Pascal Cuoq. Result graphs for an abstract interpretation-based static analyzer. In 7th Workshop on Tools for Automatic Program Analysis, 2016. [ bib ]

Back
This page was generated by bibtex2html.