| Bounding the Round-Off Error of the Upwind Scheme for Advection | 1 | 0.37 | 2022 |
| A Coq Formalization of Lebesgue Integration of Nonnegative Functions | 0 | 0.34 | 2022 |
| Emulating round-to-nearest-ties-to-zero "augmented" floating-point operations using round-to-nearest-ties-to-even arithmetic | 0 | 0.34 | 2021 |
| A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm | 0 | 0.34 | 2020 |
| Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods | 0 | 0.34 | 2020 |
| Optimal inverse projection of floating-point addition | 1 | 0.37 | 2020 |
| A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers | 0 | 0.34 | 2018 |
| On the Robustness of the 2Sum and Fast2Sum Algorithms. | 2 | 0.37 | 2017 |
| A Coq formal proof of the LaxMilgram theorem. | 1 | 0.48 | 2017 |
| Round-off Error Analysis of Explicit One-Step Numerical Integration Methods | 0 | 0.34 | 2017 |
| Formal Verification Of A Floating-Point Expansion Renormalization Algorithm | 1 | 0.35 | 2017 |
| Formalization of real analysis: a survey of proof assistants and libraries. | 11 | 1.00 | 2016 |
| Coquelicot: A User-Friendly Library of Real Analysis for Coq. | 6 | 0.62 | 2015 |
| Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number | 0 | 0.34 | 2015 |
| Verified Compilation of Floating-Point Computations | 7 | 0.47 | 2015 |
| Formal Verification of Programs Computing the Floating-Point Average. | 0 | 0.34 | 2015 |
| Trusting computations: A mechanized proof from partial differential equations to actual program | 3 | 0.59 | 2014 |
| Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program | 24 | 1.00 | 2013 |
| How to Compute the Area of a Triangle: A Formal Revisit | 1 | 0.35 | 2013 |
| A Formally-Verified C Compiler Supporting Floating-Point Arithmetic | 18 | 0.66 | 2013 |
| Improving real analysis in coq: a user-friendly approach to integrals and derivatives | 8 | 0.67 | 2012 |
| Exact and Approximated Error of the FMA | 4 | 0.76 | 2011 |
| Wave Equation Numerical Resolution: Mathematics and Program | 0 | 0.34 | 2011 |
| Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs. | 11 | 0.59 | 2011 |
| Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq | 20 | 0.89 | 2011 |
| Proofs of numerical programs when the compiler optimizes | 7 | 0.51 | 2011 |
| Formal proof of a wave equation resolution scheme: the method error | 9 | 0.62 | 2010 |
| Hardware-independent Proofs of Numerical Programs. | 12 | 0.82 | 2010 |
| Floats and Ropes: A Case Study for Formal Numerical Program Verification | 8 | 0.58 | 2009 |
| Combining Coq and Gappa for Certifying Floating-Point Programs | 26 | 1.12 | 2009 |
| Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd | 13 | 1.16 | 2008 |
| Formally Verified Argument Reduction with a Fused Multiply-Add | 0 | 0.34 | 2007 |
| Formal Verification of Floating-Point Programs | 48 | 2.55 | 2007 |
| Pitfalls of a full floating-point proof: example on the formal proof of the veltkamp/dekker algorithms | 6 | 0.74 | 2006 |
| Provably faithful evaluation of polynomials | 4 | 0.59 | 2006 |
| A simple test qualifying the accuracy of Horner's rule for polynomials | 4 | 0.69 | 2004 |
| Properties of two’s complement floating point notations | 5 | 0.78 | 2004 |
| Theorems on Efficient Argument Reductions | 10 | 1.20 | 2003 |
| Representable Correcting Terms for Possibly Underflowing Floating Point Operations | 16 | 1.56 | 2003 |
| Properties of the subtraction valid for any floating point system | 2 | 0.46 | 2002 |
| Computer validated proofs of a toolset for adaptable arithmetic | 3 | 0.54 | 2001 |
