Sylvie Boldo

Available identifiers

zbMath Open boldo.sylvieMaRDI QIDQ352947

List of research outcomes

Publication	Date of Publication	Type
Floating-point arithmetic	2023-09-12	Paper
A Coq formalization of Lebesgue induction principle and Tonelli's theorem	2023-08-17	Paper
A Coq formalization of Lebesgue integration of nonnegative functions	2022-06-09	Paper
Emulating Round-to-Nearest Ties-to-Zero “Augmented” Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic	2022-03-23	Paper
Lebesgue Induction and Tonelli's Theorem in Coq	2022-02-10	Paper
A Coq Formalization of the Bochner integral	2022-01-10	Paper
A Coq Formalization of Lebesgue Integration of Nonnegative Functions	2021-04-12	Paper
Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods	2020-12-14	Paper
Optimal inverse projection of floating-point addition	2020-02-20	Paper
Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest	2020-02-06	Paper
A Coq formalization of digital filters	2018-10-18	Paper
On the Robustness of the 2Sum and Fast2Sum Algorithms	2018-08-17	Paper
Formal verification of a floating-point expansion renormalization algorithm	2018-01-04	Paper
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd	2017-11-10	Paper
Trusting computations: a mechanized proof from partial differential equations to actual program	2017-08-21	Paper
Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven	2017-08-08	Paper
Formally Verified Argument Reduction with a Fused Multiply-Add	2017-08-08	Paper
Exact and Approximated Error of the FMA	2017-07-27	Paper
https://portal.mardi4nfdi.de/entity/Q5274886	2017-07-06	Paper
Formalization of real analysis: a survey of proof assistants and libraries	2017-04-03	Paper
Stupid is as stupid does: taking the square root of the square of a floating-point number	2016-12-16	Paper
Verified compilation of floating-point computations	2015-07-02	Paper
Coquelicot: a user-friendly library of real analysis for Coq	2015-03-25	Paper
Wave equation numerical resolution: a comprehensive mechanized proof of a C program	2013-07-05	Paper
Formal verification of numerical programs: from C annotated programs to mechanical proofs	2013-05-16	Paper
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives	2013-04-19	Paper
Formal Proof of a Wave Equation Resolution Scheme: The Method Error	2010-09-14	Paper
Computing predecessor and successor in rounding to nearest	2009-07-24	Paper
Floats and Ropes: A Case Study for Formal Numerical Program Verification	2009-07-14	Paper
Combining Coq and Gappa for Certifying Floating-Point Programs	2009-07-09	Paper
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms	2009-03-12	Paper
A simple test qualifying the accuracy of Horner's rule for polynomials	2005-09-05	Paper

Research outcomes over time

This page was built for person: Sylvie Boldo