Guillaume Melquiond

Orcid: 0000-0002-6697-1809

According to our database1, Guillaume Melquiond authored at least 48 papers between 2005 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation.
Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2023
Enabling Floating-Point Arithmetic in the Coq Proof Assistant.
J. Autom. Reason., December, 2023

Floating-point arithmetic.
Acta Numer., May, 2023

A strong call-by-need calculus.
Log. Methods Comput. Sci., 2023

WhyMP, a formally verified arbitrary-precision integer library.
J. Symb. Comput., 2023

Slimmer Formal Proofs for Mathematical Libraries.
Proceedings of the 30th IEEE Symposium on Computer Arithmetic, 2023

2021
Plotting in a Formally Verified Way.
Proceedings of the 6th Workshop on Formal Integrated Development Environment, 2021

Some Formal Tools for Computer Arithmetic: Flocq and Gappa.
Proceedings of the 28th IEEE Symposium on Computer Arithmetic, 2021

2019
Formally Verified Approximations of Definite Integrals.
J. Autom. Reason., 2019

Formal Verification of a State-of-the-Art Integer Square Root.
Proceedings of the 26th IEEE Symposium on Computer Arithmetic, 2019

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

2018
A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Handbook of Floating-Point Arithmetic (2nd Ed.).
Springer, ISBN: 978-3-319-76526-6, 2018

2017
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2017

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System.
ISTE Press, ISBN: 978-1-7854-8112-3, 2017

2016
Formalization of real analysis: a survey of proof assistants and libraries.
Math. Struct. Comput. Sci., 2016

Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq.
J. Autom. Reason., 2016

2015
Coquelicot: A User-Friendly Library of Real Analysis for Coq.
Math. Comput. Sci., 2015

Verified Compilation of Floating-Point Computations.
J. Autom. Reason., 2015

2014
Trusting computations: A mechanized proof from partial differential equations to actual program.
Comput. Math. Appl., 2014

Automating the Verification of Floating-Point Algorithms.
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....
Math. Comput., 2013

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program.
J. Autom. Reason., 2013

Preserving User Proofs across Specification Changes.
Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus.
Proceedings of the Integrated Formal Methods, 10th International Conference, 2013

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic.
Proceedings of the 21st IEEE Symposium on Computer Arithmetic, 2013

2012
Floating-point arithmetic in the Coq system.
Inf. Comput., 2012

Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers.
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011
Certifying the Floating-Point Implementation of an Elementary Function Using Gappa.
IEEE Trans. Computers, 2011

Wave Equation Numerical Resolution: Mathematics and Program
CoRR, 2011

Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq.
Proceedings of the 20th IEEE Symposium on Computer Arithmetic, 2011

2010
Certification of bounds on expressions involving rounded operators.
ACM Trans. Math. Softw., 2010

Formal Proof of a Wave Equation Resolution Scheme: The Method Error.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010


2009
Combining Coq and Gappa for Certifying Floating-Point Programs.
Proceedings of the Intelligent Computer Mathematics, 2009

IEEE Interval Standard Working Group - P1788: Current Status.
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.
IEEE Trans. Computers, 2008

Certifying floating-point implementations using Gappa
CoRR, 2008

Proving Bounds on Real-Valued Functions with Computations.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
Formally certified floating-point filters for homogeneous geometric predicates.
RAIRO Theor. Informatics Appl., 2007

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

The design of the Boost interval arithmetic library.
Theor. Comput. Sci., 2006

Assisted verification of elementary functions using Gappa.
Proceedings of the 2006 ACM Symposium on Applied Computing (SAC), 2006

A Proposal to add Interval Arithmetic to the C++ Standard Library.
Proceedings of the Reliable Implementation of Real Number Algorithms: Theory and Practice, 08.01., 2006

2005
Guaranteed Proofs Using Interval Arithmetic.
Proceedings of the 17th IEEE Symposium on Computer Arithmetic (ARITH-17 2005), 2005


  Loading...