G. Melquiond

Most-cited papers

IEEE Standard for Floating-Point Arithmetic
D. Zuras, M. Cowlishaw, A. Aiken, M. Applegate +88 more
20082,416 citations
Semantic Scholar
Handbook of Floating-Point Arithmetic (2nd Ed.)
Jean-Michel Muller, Nicolas Brunie, F. de Dinechin, C. Jeannerod +5 more
2018182 citations
Semantic Scholar
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq
S. Boldo, G. Melquiond
2011IEEE Symposium on Computer Arithmetic167 citations Open access
Semantic Scholar
Coquelicot: A User-Friendly Library of Real Analysis for Coq
S. Boldo, Catherine Lelay, G. Melquiond
2014Mathematics and Computer Science153 citations Open access
Semantic Scholar
Certification of bounds on expressions involving rounded operators
M. Daumas, G. Melquiond
2007TOMS146 citations Open access
Semantic Scholar
Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
F. de Dinechin, C. Lauter, G. Melquiond
2011IEEE transactions on computers119 citations Open access
Semantic Scholar
Assisted verification of elementary functions using Gappa
F. de Dinechin, C. Lauter, G. Melquiond
2005ACM Symposium on Applied Computing96 citations
Semantic Scholar
The design of the Boost interval arithmetic library
H. Brönnimann, G. Melquiond, Sylvain Pion
2006Theoretical Computer Science91 citations Open access
Semantic Scholar
Combining Coq and Gappa for Certifying Floating-Point Programs
S. Boldo, J. Filliâtre, G. Melquiond
2009Calculemus/MKM79 citations Open access
Semantic Scholar
Guaranteed proofs using interval arithmetic
M. Daumas, G. Melquiond, C. Muñoz
2005IEEE Symposium on Computer Arithmetic67 citations Open access
Semantic Scholar
Formalization of real analysis: a survey of proof assistants and libraries †
S. Boldo, Catherine Lelay, G. Melquiond
2015Mathematical Structures in Computer Science61 citations Open access
Semantic Scholar
Proving Bounds on Real-Valued Functions with Computations
G. Melquiond
2008International Joint Conference on Automated Reasoning60 citations Open access
Semantic Scholar
Floating-point arithmetic in the Coq system
G. Melquiond
2012Information and Computation58 citations Open access
Semantic Scholar
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd
S. Boldo, G. Melquiond
2008IEEE transactions on computers58 citations Open access
Semantic Scholar
The Boost Interval Arithmetic Library
H. Brönnimann, G. Melquiond, Sylvain Pion
200349 citations
Semantic Scholar
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
S. Boldo, Jacques-Henri Jourdan, X. Leroy, G. Melquiond
2013IEEE Symposium on Computer Arithmetic47 citations
Semantic Scholar
Verified Compilation of Floating-Point Computations
S. Boldo, Jacques-Henri Jourdan, Xavier Leroy, G. Melquiond
2014Journal of automated reasoning45 citations
Semantic Scholar
Formal Proof of a Wave Equation Resolution Scheme: The Method Error
S. Boldo, F. Clément, J. Filliâtre, Micaela Mayero +2 more
2010International Conference on Interactive Theorem Proving45 citations Open access
Semantic Scholar
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
Érik Martin-Dorel, G. Melquiond
2015Journal of automated reasoning38 citations
Semantic Scholar
Trusting computations: A mechanized proof from partial differential equations to actual program
S. Boldo, F. Clément, J. Filliâtre, Micaela Mayero +2 more
2012Computers and Mathematics with Applications38 citations Open access
Semantic Scholar
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
S. Boldo, Catherine Lelay, G. Melquiond
2012Certified Programs and Proofs29 citations Open access
Semantic Scholar
IEEE Interval Standard Working Group - P1788: Current Status
W. Edmonson, G. Melquiond
2009IEEE Symposium on Computer Arithmetic28 citations
Semantic Scholar
Floating-point arithmetic
Nicolas Brisebarre, F. de Dinechin, C. Jeannerod, V. Lefèvre +5 more
2023Acta Numerica27 citations Open access
Semantic Scholar
Theoretical Informatics and Applications Formally Certified Floating-point Filters for Homogeneous Geometric Predicates
G. Melquiond, Sylvain Pion
27 citations
Semantic Scholar
Computer Arithmetic and Formal Proofs
S. Boldo, G. Melquiond
201724 citations
Semantic Scholar
When double rounding is odd
S. Boldo, G. Melquiond
200524 citations
Semantic Scholar
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala +3 more
2012International Joint Conference on Automated Reasoning21 citations Open access
Semantic Scholar
Generating formally certified bounds on values and round-off errors
M. Daumas, G. Melquiond
200421 citations
Semantic Scholar
Computing predecessor and successor in rounding to nearest
S. Rump, P. Zimmermann, S. Boldo, G. Melquiond
200919 citations Open access
Semantic Scholar
A Proposal to add Interval Arithmetic to the C++ Standard Library
Sylvain Pion, H. Brönnimann, G. Melquiond
2006Reliable Implementation of Real Number Algorithms19 citations
Semantic Scholar
A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT
Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, G. Melquiond +1 more
2017International Conference on Computer Aided Verification18 citations Open access
Semantic Scholar
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library
Raphaël Rieu-Helft, C. Marché, G. Melquiond
2017Verified Software: Theories, Tools, Experiments17 citations Open access
Semantic Scholar
Preserving User Proofs across Specification Changes
François Bobot, J. Filliâtre, C. Marché, G. Melquiond +1 more
2013Verified Software: Theories, Tools, Experiments17 citations Open access
Semantic Scholar
Formally Verified Approximations of Definite Integrals
A. Mahboubi, G. Melquiond, T. Sibut-Pinote
2016Journal of automated reasoning16 citations Open access
Semantic Scholar
Some issues related to double rounding
Érik Martin-Dorel, G. Melquiond, J. Muller
2013BIT Numerical Mathematics16 citations
Semantic Scholar
Certifying the ﬂoating-point implementation of an elementary function using Gappa
Member Ieee Florent de Dinechin, C. Lauter, G. Melquiond, F. de Dinechin
15 citations
Semantic Scholar
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
Sylvain Conchon, G. Melquiond, Cody Roux, Mohamed Iguernelala
2012SMT@IJCAR13 citations Open access
Semantic Scholar
Formal certification of arithmetic filters for geometric predicates
G. Melquiond, Sylvain Pion
200513 citations
Semantic Scholar
Formal certiﬁcation of arithmetic ﬁlters for geometric predicates
G. Melquiond, Sylvain Pion
11 citations
Semantic Scholar
Preserving User Proofs Across Speci cation Changes ?
François Bobot, J. Filliâtre, C. Marché, G. Melquiond +1 more
20139 citations
Semantic Scholar
A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms
G. Melquiond, Raphaël Rieu-Helft
2018International Joint Conference on Automated Reasoning8 citations Open access
Semantic Scholar
WhyMP, a formally verified arbitrary-precision integer library
G. Melquiond, Raphaël Rieu-Helft
2020International Symposium on Symbolic and Algebraic Computation7 citations Open access
Semantic Scholar
Some Formal Tools for Computer Arithmetic: Flocq and Gappa
S. Boldo, G. Melquiond
2021IEEE Symposium on Computer Arithmetic6 citations
Semantic Scholar
A Strong Call-By-Need Calculus
Thibaut Balabonski, A. Lanco, G. Melquiond
2021International Conference on Formal Structures for Computation and Deduction6 citations Open access
Semantic Scholar
Formal Verification for Numerical Computations, and the Other Way Around
G. Melquiond
20195 citations
Semantic Scholar
Formal Verification of a State-of-the-Art Integer Square Root
G. Melquiond, Raphaël Rieu-Helft
2019IEEE Symposium on Computer Arithmetic5 citations Open access
Semantic Scholar
The Why3 platform 0.81
François Bobot, J. Filliâtre, C. Marché, G. Melquiond +1 more
20135 citations
Semantic Scholar
Enabling Floating-Point Arithmetic in the Coq Proof Assistant
Érik Martin-Dorel, G. Melquiond, Pierre Roux
2023Journal of automated reasoning4 citations Open access
Semantic Scholar
Deductive Program Verification
S. Boldo, G. Melquiond
20174 citations
Semantic Scholar
Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus
Daisuke Ishii, G. Melquiond, Shin Nakajima
2013International Conference on Integrated Formal Methods4 citations Open access
Semantic Scholar