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
Formally Verified Argument Reduction with a Fused Multiply-Add	2017-08-08	Paper
Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven	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

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Sylvie Boldo