| 2026 | CPP | Certifying the Decidability of the Word Problem in Monoids at Large. | Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, Finn Smith |
| 2026 | ITP | Functional Correctness of an Optimized Modular Inversion Algorithm. | Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, Toms Vallejos Parada |
| 2024 | ITP | End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. | Florian Faissole, Paul Geneau de Lamarlire, Guillaume Melquiond |
| 2023 | ARITH | Slimmer Formal Proofs for Mathematical Libraries. | Paul Geneau de Lamarlire, Guillaume Melquiond, Florian Faissole |
| 2021 | ARITH | Some Formal Tools for Computer Arithmetic: Flocq and Gappa. | Sylvie Boldo, Guillaume Melquiond |
| 2021 | FSCD | A Strong Call-By-Need Calculus. | Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond |
| 2020 | ISSAC | WhyMP, a formally verified arbitrary-precision integer library. | Guillaume Melquiond, Raphal Rieu-Helft |
| 2019 | ARITH | Formal Verification of a State-of-the-Art Integer Square Root. | Guillaume Melquiond, Raphal Rieu-Helft |
| 2018 | CADE | A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms. | Guillaume Melquiond, Raphal Rieu-Helft |
| 2017 | CAV | A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT. | Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clment Fumex |
| 2016 | ITP | Formally Verified Approximations of Definite Integrals. | Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote |
| 2013 | ARITH | A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. | Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond |
| 2013 | IFM | Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. | Daisuke Ishii, Guillaume Melquiond, Shin Nakajima |
| 2012 | CADE | A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. | Franois Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond |
| 2012 | CADE | Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. | Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala |
| 2012 | CPP | Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. | Sylvie Boldo, Catherine Lelay, Guillaume Melquiond |
| 2011 | ARITH | Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. | Sylvie Boldo, Guillaume Melquiond |
| 2010 | ITP | Formal Proof of a Wave Equation Resolution Scheme: The Method Error. | Sylvie Boldo, Franois Clment, Jean-Christophe Fillitre, Micaela Mayero, Guillaume Melquiond, Pierre Weis |
| 2009 | ARITH | IEEE Interval Standard Working Group - P1788: Current Status. | William W. Edmonson, Guillaume Melquiond |
| 2008 | CADE | Proving Bounds on Real-Valued Functions with Computations. | Guillaume Melquiond |
| 2006 | SAC | Assisted verification of elementary functions using Gappa. | Florent de Dinechin, Christoph Quirin Lauter, Guillaume Melquiond |
| 2005 | ARITH | Guaranteed Proofs Using Interval Arithmetic. | Marc Daumas, Guillaume Melquiond, Csar A. Muoz |