| 2023 | FM | A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem. | Sylvie Boldo, Franois Clment, Vincent Martin, Micaela Mayero, Houda Mouhcine |
| 2022 | ARITH | Bounding the Round-Off Error of the Upwind Scheme for Advection. | Louise Ben Salem-Knapp, Sylvie Boldo, William Weens |
| 2021 | ARITH | Some Formal Tools for Computer Arithmetic: Flocq and Gappa. | Sylvie Boldo, Guillaume Melquiond |
| 2020 | ARITH | A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm. | Sylvie Boldo, Diane Gallois-Wong, Thibault Hilaire |
| 2018 | ARITH | A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers. | Sylvie Boldo, Florian Faissole, Vincent Tourneur |
| 2017 | ARITH | Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. | Sylvie Boldo, Florian Faissole, Alexandre Chapoutot |
| 2017 | CPP | A Coq formal proof of the LaxMilgram theorem. | Sylvie Boldo, Franois Clment, Florian Faissole, Vincent Martin, Micaela Mayero |
| 2017 | ITP | Formal Verification of a Floating-Point Expansion Renormalization Algorithm. | Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu |
| 2016 | CAV | Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest. | Sylvie Boldo |
| 2015 | ICFEM | Formal Verification of Programs Computing the Floating-Point Average. | Sylvie Boldo |
| 2013 | ARITH | How to Compute the Area of a Triangle: A Formal Revisit. | Sylvie Boldo |
| 2013 | ARITH | A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. | Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond |
| 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 | ICALP | Floats and Ropes: A Case Study for Formal Numerical Program Verification. | Sylvie Boldo |
| 2007 | ARITH | Formal Verification of Floating-Point Programs. | Sylvie Boldo, Jean-Christophe Fillitre |
| 2006 | CADE | Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. | Sylvie Boldo |
| 2006 | SAC | Provably faithful evaluation of polynomials. | Sylvie Boldo, Csar A. Muoz |
| 2005 | ARITH | Some Functions Computable with a Fused-Mac. | Sylvie Boldo, Jean-Michel Muller |
| 2003 | ARITH | Representable Correcting Terms for Possibly Underflowing Floating Point Operations. | Sylvie Boldo, Marc Daumas |
| 2003 | ARITH | Theorems on Efficient Argument Reductions. | Ren-Cang Li, Sylvie Boldo, Marc Daumas |