Sylvie Boldo

Claude-Pierre Jeannerod

Acta Numer., May, 2023

A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 25th International Symposium, 2023

2022

Bounding the Round-Off Error of the Upwind Scheme for Advection.

[BibT_eX]

[DOI]

Louise Ben Salem-Knapp

William Weens

IEEE Trans. Emerg. Top. Comput., 2022

A Coq Formalization of Lebesgue Integration of Nonnegative Functions.

[BibT_eX]

[DOI]

J. Autom. Reason., 2022

Lebesgue Induction and Tonelli's Theorem in Coq.

[BibT_eX]

[DOI]

CoRR, 2022

A Coq Formalization of the Bochner integral.

[BibT_eX]

[DOI]

Louise Leclerc

CoRR, 2022

2021

Emulating Round-to-Nearest Ties-to-Zero "Augmented" Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic.

[BibT_eX]

[DOI]

Christoph Quirin Lauter

IEEE Trans. Computers, 2021

Some Formal Tools for Computer Arithmetic: Flocq and Gappa.

[BibT_eX]

[DOI]

Proceedings of the 28th IEEE Symposium on Computer Arithmetic, 2021

2020

Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods.

[BibT_eX]

[DOI]

Florian Faissole

Alexandre Chapoutot

IEEE Trans. Computers, 2020

Optimal inverse projection of floating-point addition.

[BibT_eX]

[DOI]

Diane Gallois-Wong

Pascal Cuoq

Numer. Algorithms, 2020

A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm.

[BibT_eX]

[DOI]

Diane Gallois-Wong

Thibault Hilaire

Proceedings of the 27th IEEE Symposium on Computer Arithmetic, 2020

2018

A Coq Formalization of Digital Filters.

[BibT_eX]

[DOI]

Diane Gallois-Wong

Thibault Hilaire

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers.

[BibT_eX]

[DOI]

Florian Faissole

Vincent Tourneur

Proceedings of the 25th IEEE Symposium on Computer Arithmetic, 2018

2017

On the Robustness of the 2Sum and Fast2Sum Algorithms.

[BibT_eX]

[DOI]

Stef Graillat

ACM Trans. Math. Softw., 2017

Formal Verification of a Floating-Point Expansion Renormalization Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

A Coq formal proof of the LaxMilgram theorem.

[BibT_eX]

[DOI]

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

Round-off Error Analysis of Explicit One-Step Numerical Integration Methods.

[BibT_eX]

[DOI]

Florian Faissole

Alexandre Chapoutot

Proceedings of the 24th IEEE Symposium on Computer Arithmetic, 2017

Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System.

[BibT_eX]

[DOI]

ISTE Press, ISBN: 978-1-7854-8112-3, 2017

2016

Formalization of real analysis: a survey of proof assistants and libraries.

[BibT_eX]

[DOI]

Catherine Lelay

Math. Struct. Comput. Sci., 2016

Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest.

[BibT_eX]

[DOI]

Proceedings of the Numerical Software Verification - 9th International Workshop, 2016

2015

Coquelicot: A User-Friendly Library of Real Analysis for Coq.

[BibT_eX]

[DOI]

Catherine Lelay

Math. Comput. Sci., 2015

Verified Compilation of Floating-Point Computations.

[BibT_eX]

[DOI]

Jacques-Henri Jourdan

Xavier Leroy

J. Autom. Reason., 2015

Formal Verification of Programs Computing the Floating-Point Average.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2015

2014

Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number.

[BibT_eX]

[DOI]

Proceedings of the Seventh and Eighth International Workshops on Numerical Software Verification, 2014

Trusting computations: A mechanized proof from partial differential equations to actual program.

[BibT_eX]

[DOI]

Comput. Math. Appl., 2014

Deductive Formal Verification: How To Make Your Floating-Point Programs Behave.

[BibT_eX]

[DOI]

, 2014

2013

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic.

[BibT_eX]

[DOI]

Jacques-Henri Jourdan

Xavier Leroy

Proceedings of the 21st IEEE Symposium on Computer Arithmetic, 2013

How to Compute the Area of a Triangle: A Formal Revisit.

[BibT_eX]

[DOI]

Proceedings of the 21st IEEE Symposium on Computer Arithmetic, 2013

2012

Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives.

[BibT_eX]

[DOI]

Catherine Lelay

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

Exact and Approximated Error of the FMA.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2011

Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs.

[BibT_eX]

[DOI]

Claude Marché

Math. Comput. Sci., 2011

Proofs of numerical programs when the compiler optimizes.

[BibT_eX]

[DOI]

Thi Minh Tuyen Nguyen

Innov. Syst. Softw. Eng., 2011

Wave Equation Numerical Resolution: Mathematics and Program

[BibT_eX]

[DOI]

CoRR, 2011

Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE Symposium on Computer Arithmetic, 2011

2010

Hardware-independent Proofs of Numerical Programs.

[BibT_eX]

Thi Minh Tuyen Nguyen

Proceedings of the Second NASA Formal Methods Symposium, 2010

Formal Proof of a Wave Equation Resolution Scheme: The Method Error.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

2009

Formally Verified Argument Reduction with a Fused Multiply-Add.

[BibT_eX]

[DOI]

Ren-Cang Li

IEEE Trans. Computers, 2009

Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2009

Combining Coq and Gappa for Certifying Floating-Point Programs.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2009

Floats and Ropes: A Case Study for Formal Numerical Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 36th Internatilonal Colloquium, 2009

2008

Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2008

2007

Formal Verification of Floating-Point Programs.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Symposium on Computer Arithmetic (ARITH-18 2007), 2007

2006

Provably faithful evaluation of polynomials.

[BibT_eX]

[DOI]

César A. Muñoz

Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), 2006

Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Some Functions Computable with a Fused-Mac.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE Symposium on Computer Arithmetic (ARITH-17 2005), 2005

2004

Properties of two's complement floating point notations.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2004

A Simple Test Qualifying the Accuracy of Horner'S Rule for Polynomials.

[BibT_eX]

[DOI]

Numer. Algorithms, 2004

2003

Theorems on Efficient Argument Reductions.

[BibT_eX]

[DOI]

Ren-Cang Li

Proceedings of the 16th IEEE Symposium on Computer Arithmetic (Arith-16 2003), 2003

Representable Correcting Terms for Possibly Underflowing Floating Point Operations.

[BibT_eX]

[DOI]

Proceedings of the 16th IEEE Symposium on Computer Arithmetic (Arith-16 2003), 2003

2002

Properties of the subtraction valid for any floating point system.

[BibT_eX]

[DOI]