| Publication | Date of Publication | Type |
|---|
Floating-point arithmetic
Acta Numerica | 2023-09-12 | Paper |
A Coq formalization of Lebesgue induction principle and Tonelli's theorem
Formal Methods | 2023-08-17 | Paper |
A Coq formalization of Lebesgue integration of nonnegative functions
Journal of Automated Reasoning | 2022-06-09 | Paper |
Emulating Round-to-Nearest Ties-to-Zero “Augmented” Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic
IEEE Transactions on Computers | 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
(available as arXiv preprint) | 2021-04-12 | Paper |
Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods
IEEE Transactions on Computers | 2020-12-14 | Paper |
Optimal inverse projection of floating-point addition
Numerical Algorithms | 2020-02-20 | Paper |
Computing a correct and tight rounding error bound using rounding-to-nearest
Numerical Software Verification | 2020-02-06 | Paper |
| A Coq formalization of digital filters | 2018-10-18 | Paper |
On the robustness of the 2Sum and Fast2Sum algorithms
ACM Transactions on Mathematical Software | 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
IEEE Transactions on Computers | 2017-11-10 | Paper |
Trusting computations: a mechanized proof from partial differential equations to actual program
Computers & Mathematics with Applications | 2017-08-21 | Paper |
Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven
IEEE Transactions on Computers | 2017-08-08 | Paper |
Formally Verified Argument Reduction with a Fused Multiply-Add
IEEE Transactions on Computers | 2017-08-08 | Paper |
Exact and Approximated Error of the FMA
IEEE Transactions on Computers | 2017-07-27 | Paper |
| Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system | 2017-07-06 | Paper |
Formalization of real analysis: a survey of proof assistants and libraries
Mathematical Structures in Computer Science | 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
Journal of Automated Reasoning | 2015-07-02 | Paper |
Coquelicot: a user-friendly library of real analysis for Coq
Mathematics in Computer Science | 2015-03-25 | Paper |
Wave equation numerical resolution: a comprehensive mechanized proof of a C program
Journal of Automated Reasoning | 2013-07-05 | Paper |
Formal verification of numerical programs: from C annotated programs to mechanical proofs
Mathematics in Computer Science | 2013-05-16 | Paper |
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
Certified Programs and Proofs | 2013-04-19 | Paper |
Formal proof of a wave equation resolution scheme: the method error
Interactive Theorem Proving | 2010-09-14 | Paper |
Computing predecessor and successor in rounding to nearest
BIT | 2009-07-24 | Paper |
Floats and Ropes: A Case Study for Formal Numerical Program Verification
Automata, Languages and Programming | 2009-07-14 | Paper |
Combining Coq and Gappa for Certifying Floating-Point Programs
Lecture Notes in Computer Science | 2009-07-09 | Paper |
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms
Automated Reasoning | 2009-03-12 | Paper |
A simple test qualifying the accuracy of Horner's rule for polynomials
Numerical Algorithms | 2005-09-05 | Paper |
