Sylvie Boldo

Publication Activity (10 Years)

Years Active: 2001-2024
Publications (10 Years): 26

Top Topics

Formal Verification

Partial Differential Equations

Top Venues

IEEE Trans. Computers

J. Autom. Reason.

Publications

Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, Pierre Rousselin
Teaching Divisibility and Binomials with Coq. CoRR (2024)
Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem. FM (2023)
Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller
Floating-point arithmetic. Acta Numer. 32 (2023)
Louise Ben Salem-Knapp, Sylvie Boldo, William Weens
Bounding the Round-Off Error of the Upwind Scheme for Advection. IEEE Trans. Emerg. Top. Comput. 10 (3) (2022)
Sylvie Boldo, François Clément, Louise Leclerc
A Coq Formalization of the Bochner integral. CoRR (2022)
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
A Coq Formalization of Lebesgue Integration of Nonnegative Functions. J. Autom. Reason. 66 (2) (2022)
Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
Lebesgue Induction and Tonelli's Theorem in Coq. CoRR (2022)
Louise Ben Salem-Knapp, Sylvie Boldo, William Weens
Bounding the Round-Off Error of the Upwind Scheme for Advection. ARITH (2022)
Sylvie Boldo, Guillaume Melquiond
Some Formal Tools for Computer Arithmetic: Flocq and Gappa. ARITH (2021)
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
A Coq Formalization of Lebesgue Integration of Nonnegative Functions. CoRR (2021)
Sylvie Boldo, Christoph Quirin Lauter, Jean-Michel Muller
Emulating Round-to-Nearest Ties-to-Zero "Augmented" Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic. IEEE Trans. Computers 70 (7) (2021)
Sylvie Boldo, Diane Gallois-Wong, Thibault Hilaire
A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm. ARITH (2020)
Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods. IEEE Trans. Computers 69 (12) (2020)
Diane Gallois-Wong, Sylvie Boldo, Pascal Cuoq
Optimal inverse projection of floating-point addition. Numer. Algorithms 83 (3) (2020)
Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire
A Coq Formalization of Digital Filters. CICM (2018)
Sylvie Boldo, Florian Faissole, Vincent Tourneur
A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers. ARITH (2018)
Sylvie Boldo, Stef Graillat, Jean-Michel Muller
On the Robustness of the 2Sum and Fast2Sum Algorithms. ACM Trans. Math. Softw. 44 (1) (2017)
Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
A Coq formal proof of the LaxMilgram theorem. CPP (2017)
Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu
Formal Verification of a Floating-Point Expansion Renormalization Algorithm. ITP (2017)
Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. ARITH (2017)
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26 (7) (2016)
Sylvie Boldo
Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest. NSV@CAV (2016)
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
Coquelicot: A User-Friendly Library of Real Analysis for Coq. Math. Comput. Sci. 9 (1) (2015)
Sylvie Boldo
Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number. Electron. Notes Theor. Comput. Sci. 317 (2015)
Sylvie Boldo
Formal Verification of Programs Computing the Floating-Point Average. ICFEM (2015)
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
Verified Compilation of Floating-Point Computations. J. Autom. Reason. 54 (2) (2015)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Trusting computations: A mechanized proof from partial differential equations to actual program. Comput. Math. Appl. 68 (3) (2014)
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. IEEE Symposium on Computer Arithmetic (2013)
Sylvie Boldo
How to Compute the Area of a Triangle: A Formal Revisit. IEEE Symposium on Computer Arithmetic (2013)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. J. Autom. Reason. 50 (4) (2013)
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. CPP (2012)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. CoRR (2012)
Sylvie Boldo, Guillaume Melquiond
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. IEEE Symposium on Computer Arithmetic (2011)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Wave Equation Numerical Resolution: Mathematics and Program CoRR (2011)
Sylvie Boldo, Claude Marché
Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs. Math. Comput. Sci. 5 (4) (2011)
Sylvie Boldo, Jean-Michel Muller
Exact and Approximated Error of the FMA. IEEE Trans. Computers 60 (2) (2011)
Sylvie Boldo, Thi Minh Tuyen Nguyen
Proofs of numerical programs when the compiler optimizes. Innov. Syst. Softw. Eng. 7 (2) (2011)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Formal Proof of a Wave Equation Resolution Scheme: the Method Error CoRR (2010)
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. ITP (2010)
Sylvie Boldo, Thi Minh Tuyen Nguyen
Hardware-independent Proofs of Numerical Programs. NASA Formal Methods (2010)
Sylvie Boldo
Floats and Ropes: A Case Study for Formal Numerical Program Verification. ICALP (2) (2009)
Sylvie Boldo, Marc Daumas, Ren-Cang Li
Formally Verified Argument Reduction with a Fused Multiply-Add. IEEE Trans. Computers 58 (8) (2009)
Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
Combining Coq and Gappa for Certifying Floating-Point Programs. Calculemus/MKM (2009)
Sylvie Boldo
Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven. IEEE Trans. Computers 58 (2) (2009)
Sylvie Boldo, Guillaume Melquiond
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Trans. Computers 57 (4) (2008)
Sylvie Boldo, Jean-Christophe Filliâtre
Formal Verification of Floating-Point Programs. IEEE Symposium on Computer Arithmetic (2007)
Sylvie Boldo, Marc Daumas, Ren-Cang Li
Formally Verified Argument Reduction with a Fused-Multiply-Add CoRR (2007)
Sylvie Boldo, César A. Muñoz
Provably faithful evaluation of polynomials. SAC (2006)
Sylvie Boldo
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. IJCAR (2006)
Sylvie Boldo, Jean-Michel Muller
Some Functions Computable with a Fused-Mac. IEEE Symposium on Computer Arithmetic (2005)
Sylvie Boldo, Marc Daumas
A Simple Test Qualifying the Accuracy of Horner'S Rule for Polynomials. Numer. Algorithms 37 (1-4) (2004)
Sylvie Boldo, Marc Daumas
Properties of two's complement floating point notations. Int. J. Softw. Tools Technol. Transf. 5 (2-3) (2004)
Sylvie Boldo, Marc Daumas
Representable Correcting Terms for Possibly Underflowing Floating Point Operations. IEEE Symposium on Computer Arithmetic (2003)
Ren-Cang Li, Sylvie Boldo, Marc Daumas
Theorems on Efficient Argument Reductions. IEEE Symposium on Computer Arithmetic (2003)
Sylvie Boldo, Marc Daumas
Properties of the subtraction valid for any floating point system. Electron. Notes Theor. Comput. Sci. 66 (2) (2002)
Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Théry
Computer validated proofs of a toolset for adaptable arithmetic CoRR (2001)