Guillaume Melquiond

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2023

Enabling Floating-Point Arithmetic in the Coq Proof Assistant.

[BibT_eX]

[DOI]

Érik Martin-Dorel

Pierre Roux

J. Autom. Reason., December, 2023

Floating-point arithmetic.

[BibT_eX]

[DOI]

Claude-Pierre Jeannerod

Jean-Michel Muller

Acta Numer., May, 2023

A strong call-by-need calculus.

[BibT_eX]

[DOI]

Thibaut Balabonski

Antoine Lanco

Log. Methods Comput. Sci., 2023

WhyMP, a formally verified arbitrary-precision integer library.

[BibT_eX]

[DOI]

Paul Geneau de Lamarlière

J. Symb. Comput., 2023

Slimmer Formal Proofs for Mathematical Libraries.

[BibT_eX]

[DOI]

Florian Faissole

Proceedings of the 30th IEEE Symposium on Computer Arithmetic, 2023

2021

Plotting in a Formally Verified Way.

[BibT_eX]

[DOI]

Proceedings of the 6th Workshop on Formal Integrated Development Environment, 2021

Some Formal Tools for Computer Arithmetic: Flocq and Gappa.

[BibT_eX]

[DOI]

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

2019

Formally Verified Approximations of Definite Integrals.

[BibT_eX]

[DOI]

Assia Mahboubi

Thomas Sibut-Pinote

J. Autom. Reason., 2019

Formal Verification of a State-of-the-Art Integer Square Root.

[BibT_eX]

[DOI]

Proceedings of the 26th IEEE Symposium on Computer Arithmetic, 2019

Formal Verification for Numerical Computations, and the Other Way Around.

[BibT_eX]

[DOI]

, 2019

2018

A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Handbook of Floating-Point Arithmetic (2nd Ed.).

[BibT_eX]

[DOI]

Jean-Michel Muller

Nicolas Brunie

Claude-Pierre Jeannerod

Springer, ISBN: 978-3-319-76526-6, 2018

2017

How to Get an Efficient yet Verified Arbitrary-Precision Integer Library.

[BibT_eX]

[DOI]

Claude Marché

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2017

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 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

Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq.

[BibT_eX]

[DOI]

Érik Martin-Dorel

J. Autom. Reason., 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

2014

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

[BibT_eX]

[DOI]

Comput. Math. Appl., 2014

Automating the Verification of Floating-Point Algorithms.

[BibT_eX]

[DOI]

Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, 2014

2013

Numerical approximation of The Masser-Gramain constant to four decimal digits: δ = 1.819....

[BibT_eX]

[DOI]

W. Georg Nowak

Paul Zimmermann

Math. Comput., 2013

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

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

Preserving User Proofs across Specification Changes.

[BibT_eX]

[DOI]

François Bobot

Claude Marché

Andrei Paskevich

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus.

[BibT_eX]

[DOI]

Daisuke Ishii

Shin Nakajima

Proceedings of the Integrated Formal Methods, 10th International Conference, 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

2012

Floating-point arithmetic in the Coq system.

[BibT_eX]

[DOI]

Inf. Comput., 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

Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers.

[BibT_eX]

[DOI]

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

Certifying the Floating-Point Implementation of an Elementary Function Using Gappa.

[BibT_eX]

[DOI]

Christoph Quirin Lauter

IEEE Trans. Computers, 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

Certification of bounds on expressions involving rounded operators.

[BibT_eX]

[DOI]

Marc Daumas

ACM Trans. Math. Softw., 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

Handbook of Floating-Point Arithmetic.

[BibT_eX]

[DOI]

Jean-Michel Muller

Nicolas Brisebarre

Claude-Pierre Jeannerod

Birkhäuser, ISBN: 978-0-8176-4704-9, 2010

2009

Combining Coq and Gappa for Certifying Floating-Point Programs.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2009

IEEE Interval Standard Working Group - P1788: Current Status.

[BibT_eX]

[DOI]

William W. Edmonson

Proceedings of the 19th IEEE Symposium on Computer Arithmetic, 2009

2008

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

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2008

Certifying floating-point implementations using Gappa

[BibT_eX]

[DOI]

Christoph Quirin Lauter

CoRR, 2008

Proving Bounds on Real-Valued Functions with Computations.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

Formally certified floating-point filters for homogeneous geometric predicates.

[BibT_eX]

[DOI]

Sylvain Pion

RAIRO Theor. Informatics Appl., 2007

2006

De l'arithmétique d'intervalles à la certification de programmes. (From interval arithmetic to program verification).

[BibT_eX]

[DOI]

PhD thesis, 2006

The design of the Boost interval arithmetic library.

[BibT_eX]

[DOI]

Hervé Brönnimann

Sylvain Pion

Theor. Comput. Sci., 2006

Assisted verification of elementary functions using Gappa.

[BibT_eX]

[DOI]

Christoph Quirin Lauter

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

A Proposal to add Interval Arithmetic to the C++ Standard Library.

[BibT_eX]

[DOI]

Sylvain Pion

Hervé Brönnimann

Proceedings of the Reliable Implementation of Real Number Algorithms: Theory and Practice, 08.01., 2006

2005

Guaranteed Proofs Using Interval Arithmetic.

[BibT_eX]

[DOI]

Marc Daumas