Publications 2023
BackBooks / Journals / Conferences / PhD theses / Misc. / Reports
Books and book chapters
Journals
| [5] | 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 ] |
| [4] | Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, and Lars Birkedal. Cerise: Program verification on a capability machine in the presence of untrusted code. Journal of the ACM, 2023. [ bib | DOI | full text on HAL ] |
| [3] | Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, and Jean-Michel Muller. Floating-point arithmetic. Acta Numerica, 32:203--290, 2023. [ bib | DOI | full text on HAL ] |
| [2] | Érik Martin-Dorel, Guillaume Melquiond, and Pierre Roux. Enabling floating-point arithmetic in the Coq proof assistant. Journal of Automated Reasoning, 67(33), 2023. [ bib | DOI | full text on HAL ] |
| [1] | Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A strong call-by-need calculus. Logical Methods in Computer Science, 19(1), 2023. [ bib | DOI | full text on HAL ] |
Conferences
| [4] | Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. A Coq formalization of Lebesgue induction principle and Tonelli's theorem. In 25th International Symposium on Formal Methods (FM 2023), volume 14000 of Lecture Notes in Computer Science, pages 39--55, 2023. [ bib | DOI | full text on HAL ] |
| [3] | Jean-Christophe Filliâtre and Andrei Paskevich. L'arithmétique de séparation. In Timothy Bourke and Delphine Demange, editors, JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, pages 274--283, 2023. [ bib | full text on HAL ] |
| [2] | Paul Geneau de Lamarlière, Guillaume Melquiond, and Florian Faissole. Slimmer formal proofs for mathematical libraries. In Int. Conf. on Computer Arithmetic, 2023. [ bib | full text on HAL ] |
| [1] | Sylvain Conchon and Alexandrina Korneva. The cubicle fuzzy loop: A fuzzing-based extension for the Cubicle model checker. In Carla Ferreira and Tim A. C. Willemse, editors, Software Engineering and Formal Method, volume 14323 of Lecture Notes in Computer Science, pages 30--46. Springer, 2023. [ bib | DOI | full text on HAL ] |
PhD theses
| [3] | Clément Pascutto. Runtime Verification of OCaml Programs. Phd thesis, Université Paris-Saclay, 2023. [ bib ] |
| [2] | Xavier Denis. Deductive Verification of Rust Programs. Phd thesis, Université Paris-Saclay, 2023. [ bib ] |
| [1] | Antoine Lanco. Stratégies pour la réduction forte. Phd thesis, Université Paris-Saclay, 2023. [ bib ] |
Misc.
Reports
| [2] | 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 ] |
| [1] | Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. Lebesgue induction and Tonelli's theorem in Coq. Research Report 9457, Inria, 2023. [ bib | full text on HAL ] |
Back
Books / Journals / Conferences / PhD theses / Misc. / Reports
This page was generated by bibtex2html.