Computer validated proofs of a toolset for adaptable arithmetic - Sylvie Boldo; Marc Daumas; Claire Moreau-Finot; Laurent Théry (CoRR, 2001)

Properties of the subtraction valid for any floating point system. - Sylvie Boldo; Marc Daumas (FMICS, 2002)

Representable Correcting Terms for Possibly Underflowing Floating Point Operations. - Sylvie Boldo; Marc Daumas (IEEE Symposium on Computer Arithmetic, 2003)

Theorems on Efficient Argument Reductions. - Ren-Cang Li; Sylvie Boldo; Marc Daumas (IEEE Symposium on Computer Arithmetic, 2003)

A Simple Test Qualifying the Accuracy of Horner'S Rule for Polynomials. - Sylvie Boldo; Marc Daumas (Numer. Algorithms, 2004)

Properties of two's complement floating point notations. - Sylvie Boldo; Marc Daumas (Int. J. Softw. Tools Technol. Transf., 2004)

Some Functions Computable with a Fused-Mac. - Sylvie Boldo; Jean-Michel Muller (IEEE Symposium on Computer Arithmetic, 2005)

Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. - Sylvie Boldo (IJCAR, 2006)

Provably faithful evaluation of polynomials. - Sylvie Boldo; César A. Muñoz (SAC, 2006)

Formal Verification of Floating-Point Programs. - Sylvie Boldo; Jean-Christophe Filliâtre (IEEE Symposium on Computer Arithmetic, 2007)

Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd. - Sylvie Boldo; Guillaume Melquiond (IEEE Trans. Computers, 2008)

Floats and Ropes: A Case Study for Formal Numerical Program Verification. - Sylvie Boldo (ICALP (2), 2009)

Combining Coq and Gappa for Certifying Floating-Point Programs. - Sylvie Boldo; Jean-Christophe Filliâtre; Guillaume Melquiond (Calculemus/MKM, 2009)

Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven. - Sylvie Boldo (IEEE Trans. Computers, 2009)

Formally Verified Argument Reduction with a Fused Multiply-Add. - Sylvie Boldo; Marc Daumas; Ren-Cang Li (IEEE Trans. Computers, 2009)

Formal Proof of a Wave Equation Resolution Scheme: The Method Error. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (ITP, 2010)

Hardware-independent Proofs of Numerical Programs. - Sylvie Boldo; Thi Minh Tuyen Nguyen (NASA Formal Methods, 2010)

Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. - Sylvie Boldo; Guillaume Melquiond (IEEE Symposium on Computer Arithmetic, 2011)

Wave Equation Numerical Resolution: Mathematics and Program - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (CoRR, 2011)

Proofs of numerical programs when the compiler optimizes. - Sylvie Boldo; Thi Minh Tuyen Nguyen (Innov. Syst. Softw. Eng., 2011)

Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs. - Sylvie Boldo; Claude Marché (Math. Comput. Sci., 2011)

Exact and Approximated Error of the FMA. - Sylvie Boldo; Jean-Michel Muller (IEEE Trans. Computers, 2011)

Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. - Sylvie Boldo; Catherine Lelay; Guillaume Melquiond (CPP, 2012)

How to Compute the Area of a Triangle: A Formal Revisit. - Sylvie Boldo (IEEE Symposium on Computer Arithmetic, 2013)

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. - Sylvie Boldo; Jacques-Henri Jourdan; Xavier Leroy; Guillaume Melquiond (IEEE Symposium on Computer Arithmetic, 2013)

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (J. Autom. Reason., 2013)

Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. - Sylvie Boldo (2014)

Trusting computations: A mechanized proof from partial differential equations to actual program. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (Comput. Math. Appl., 2014)

Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number. - Sylvie Boldo (NSV, 2014)

Formal Verification of Programs Computing the Floating-Point Average. - Sylvie Boldo (ICFEM, 2015)

Verified Compilation of Floating-Point Computations. - Sylvie Boldo; Jacques-Henri Jourdan; Xavier Leroy; Guillaume Melquiond (J. Autom. Reason., 2015)

Coquelicot: A User-Friendly Library of Real Analysis for Coq. - Sylvie Boldo; Catherine Lelay; Guillaume Melquiond (Math. Comput. Sci., 2015)

Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest. - Sylvie Boldo (NSV@CAV, 2016)

Formalization of real analysis: a survey of proof assistants and libraries. - Sylvie Boldo; Catherine Lelay; Guillaume Melquiond (Math. Struct. Comput. Sci., 2016)

Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System. - Sylvie Boldo; Guillaume Melquiond (ISTE Press, 2017)

Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. - Sylvie Boldo; Florian Faissole; Alexandre Chapoutot (ARITH, 2017)

A Coq formal proof of the LaxMilgram theorem. - Sylvie Boldo; François Clément; Florian Faissole; Vincent Martin; Micaela Mayero (CPP, 2017)

Formal Verification of a Floating-Point Expansion Renormalization Algorithm. - Sylvie Boldo; Mioara Joldes; Jean-Michel Muller; Valentina Popescu (ITP, 2017)

On the Robustness of the 2Sum and Fast2Sum Algorithms. - Sylvie Boldo; Stef Graillat; Jean-Michel Muller (ACM Trans. Math. Softw., 2017)

A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers. - Sylvie Boldo; Florian Faissole; Vincent Tourneur (ARITH, 2018)

A Coq Formalization of Digital Filters. - Diane Gallois-Wong; Sylvie Boldo; Thibault Hilaire (CICM, 2018)

A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm. - Sylvie Boldo; Diane Gallois-Wong; Thibault Hilaire (ARITH, 2020)

Optimal inverse projection of floating-point addition. - Diane Gallois-Wong; Sylvie Boldo; Pascal Cuoq (Numer. Algorithms, 2020)

Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods. - Sylvie Boldo; Florian Faissole; Alexandre Chapoutot (IEEE Trans. Computers, 2020)

Some Formal Tools for Computer Arithmetic: Flocq and Gappa. - Sylvie Boldo; Guillaume Melquiond (ARITH, 2021)

Emulating Round-to-Nearest Ties-to-Zero "Augmented" Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic. - Sylvie Boldo; Christoph Quirin Lauter; Jean-Michel Muller (IEEE Trans. Computers, 2021)

A Coq Formalization of the Bochner integral. - Sylvie Boldo; François Clément; Louise Leclerc (CoRR, 2022)

Lebesgue Induction and Tonelli's Theorem in Coq. - Sylvie Boldo; François Clément; Vincent Martin; Micaela Mayero; Houda Mouhcine (CoRR, 2022)

A Coq Formalization of Lebesgue Integration of Nonnegative Functions. - Sylvie Boldo; François Clément; Florian Faissole; Vincent Martin; Micaela Mayero (J. Autom. Reason., 2022)

Bounding the Round-Off Error of the Upwind Scheme for Advection. - Louise Ben Salem-Knapp; Sylvie Boldo; William Weens (IEEE Trans. Emerg. Top. Comput., 2022)

A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem. - Sylvie Boldo; François Clément; Vincent Martin; Micaela Mayero; Houda Mouhcine (FM, 2023)

Floating-point arithmetic. - Sylvie Boldo; Claude-Pierre Jeannerod; Guillaume Melquiond; Jean-Michel Muller (Acta Numer., 2023)

Teaching Divisibility and Binomials with Coq. - Sylvie Boldo; François Clément; David Hamelin; Micaela Mayero; Pierre Rousselin (ThEdu@CADE, 2024)