| Publication | Date of Publication | Type |
|---|
| End-to-end formal verification of a fast and accurate floating-point approximation | 2026-02-10 | Paper |
Enabling floating-point arithmetic in the Coq proof assistant
Journal of Automated Reasoning | 2023-10-24 | Paper |
Floating-point arithmetic
Acta Numerica | 2023-09-12 | Paper |
A strong call-by-need calculus
Logical Methods in Computer Science | 2023-08-26 | Paper |
| A strong call-by-need calculus | 2023-06-23 | Paper |
WhyMP, a formally verified arbitrary-precision integer library
Journal of Symbolic Computation | 2022-09-22 | Paper |
| A three-tier strategy for reasoning about floating-point numbers in SMT | 2022-08-12 | Paper |
WhyMP, a formally verified arbitrary-precision integer library
Proceedings of the 45th International Symposium on Symbolic and Algebraic Computation | 2021-01-22 | Paper |
Formally verified approximations of definite integrals
Journal of Automated Reasoning | 2019-02-18 | Paper |
| How to get an efficient yet verified arbitrary-precision integer library | 2018-12-07 | Paper |
| A Why3 framework for reflection proofs and its application to GMP's algorithms | 2018-10-18 | Paper |
| Handbook of floating-point arithmetic | 2018-04-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 |
Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
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 |
Certification of bounds on expressions involving rounded operators
ACM Transactions on Mathematical Software | 2017-05-19 | Paper |
Formalization of real analysis: a survey of proof assistants and libraries
Mathematical Structures in Computer Science | 2017-04-03 | Paper |
Proving tight bounds on univariate expressions with elementary functions in Coq
Journal of Automated Reasoning | 2016-10-27 | Paper |
Formally verified approximations of definite integrals
Interactive Theorem Proving | 2016-10-27 | 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 |
Some issues related to double rounding
BIT | 2014-02-03 | Paper |
Wave equation numerical resolution: a comprehensive mechanized proof of a C program
Journal of Automated Reasoning | 2013-07-05 | Paper |
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
Certified Programs and Proofs | 2013-04-19 | Paper |
Numerical approximation of the Masser-Gramain constant to four decimal digits: \(\delta= 1.819\dots\)
Mathematics of Computation | 2013-03-20 | Paper |
Floating-point arithmetic in the Coq system
Information and Computation | 2012-10-11 | Paper |
A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic
Automated Reasoning | 2012-09-05 | 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 |
Combining Coq and Gappa for Certifying Floating-Point Programs
Lecture Notes in Computer Science | 2009-07-09 | Paper |
| Handbook of Floating-Point Arithmetic | 2009-05-26 | Paper |
Proving Bounds on Real-Valued Functions with Computations
Automated Reasoning | 2008-11-27 | Paper |
Formally certified floating-point filters for homogeneous geometric predicates
RAIRO - Theoretical Informatics and Applications | 2008-02-22 | Paper |
Formally certified floating-point filters for homogeneous geometric predicates
RAIRO - Theoretical Informatics and Applications | 2008-02-22 | Paper |
The design of the Boost interval arithmetic library
Theoretical Computer Science | 2006-03-20 | Paper |
