Suivre
Guillaume Melquiond
Guillaume Melquiond
Inria, University Paris Saclay
Adresse e-mail validée de inria.fr - Page d'accueil
Titre
Citée par
Citée par
Année
Handbook of floating-point arithmetic
JM Muller, N Brisebarre, F De Dinechin, CP Jeannerod, L Vincent, ...
Birkhauser, 2009
1042*2009
IEEE Standard for Floating-Point Arithmetic
D Zuras, M Cowlishaw, A Aiken, M Applegate, D Bailey, S Bass, ...
IEEE Std 754-2008, 1-70, 2008
3262008
Flocq: A unified library for proving floating-point algorithms in Coq
S Boldo, G Melquiond
20th IEEE Symposium on Computer Arithmetic, 243-252, 2010
2002010
Certification of bounds on expressions involving rounded operators
M Daumas, G Melquiond
Transactions on Mathematical Software 37 (1), 1-20, 2010
1612010
Coquelicot: A user-friendly library of real analysis for Coq
S Boldo, C Lelay, G Melquiond
Mathematics in Computer Science 9, 41-62, 2015
1562015
Certifying the floating-point implementation of an elementary function using Gappa
F De Dinechin, C Lauter, G Melquiond
Transactions on Computers 60 (2), 242-253, 2011
1502011
Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program
S Boldo, F Clément, JC Filliâtre, M Mayero, G Melquiond, P Weis
Journal of Automated Reasoning, 2013
1152013
Assisted verification of elementary functions using Gappa
F De Dinechin, CQ Lauter, G Melquiond
Proceedings of the 2006 ACM symposium on Applied computing, 1318-1322, 2006
1152006
Combining Coq and Gappa for certifying floating-point programs
S Boldo, JC Filliâtre, G Melquiond
International Conference on Intelligent Computer Mathematics, 59-74, 2009
1012009
The design of the Boost interval arithmetic library
H Brönnimann, G Melquiond, S Pion
Theoretical Computer Science 351 (1), 111-118, 2006
932006
Formalization of real analysis: A survey of proof assistants and libraries
S Boldo, C Lelay, G Melquiond
Mathematical Structures in Computer Science 26 (7), 1196-1233, 2016
822016
Guaranteed proofs using interval arithmetic
M Daumas, G Melquiond, C Munoz
17th IEEE Symposium on Computer Arithmetic, 188-195, 2005
782005
Floating-point arithmetic in the Coq system
G Melquiond
Information and Computation 216, 14-23, 2012
672012
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
S Boldo, JH Jourdan, X Leroy, G Melquiond
21st IEEE Symposium on Computer Arithmetic (ARITH), 107-115, 2013
662013
Proving bounds on real-valued functions with computations
G Melquiond
International Joint Conference on Automated Reasoning, 2-17, 2008
662008
Emulation of a FMA and correctly rounded sums: Proved algorithms using rounding to odd
S Boldo, G Melquiond
IEEE Transactions on Computers 57 (4), 462-471, 2008
662008
Verified compilation of floating-point computations
S Boldo, JH Jourdan, X Leroy, G Melquiond
Journal of Automated Reasoning 54, 135-163, 2015
622015
Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System
S Boldo, G Melquiond
Elsevier, 2017
582017
Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program
S Boldo, F Clément, JC Filliâtre, M Mayero, G Melquiond, P Weis
532012
Formal proof of a wave equation resolution scheme: the method error
S Boldo, F Clément, JC Filliâtre, M Mayero, G Melquiond, P Weis
International Conference on Interactive Theorem Proving, 147-162, 2010
532010
Le système ne peut pas réaliser cette opération maintenant. Veuillez réessayer plus tard.
Articles 1–20