Guillaume Melquiond

Cited by

	All	Since 2019
Citations	3612	1646
h-index	27	19
i10-index	44	29

400

200

100

300

2005200620072008200920102011201220132014201520162017201820192020202120222023202415 76 46 46 45 97 114 139 158 201 210 212 247 275 391 252 268 238 269 226

Public access

View all

8 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Florent de Dinechinprofessor, INSA-LyonVerified email at insa-lyon.fr
Sylvie BoldoInria, LMF, University Paris SaclayVerified email at inria.fr
jean-michel mullerCNRS, Ecole Normale Supérieure de Lyon, INRIA, Université de LyonVerified email at ens-lyon.fr
Vincent LefèvreINRIA / LIPVerified email at vinc17.net
Nathalie RevolResearch Scientist, INRIA, LIP-ENS de Lyon, FranceVerified email at ens-lyon.fr
Claude-Pierre JeannerodResearcher at Inria (ENS de Lyon, France)Verified email at ens-lyon.fr
Damien StehléCryptoLabVerified email at cryptolab.co.kr
Sylvain Pionex-INRIAVerified email at inria.fr
Jean-Christophe FilliâtreCNRSVerified email at lri.fr
Marc DaumasProfesseur d'informatique, Université de Perpignan, Laboratoire PROMESVerified email at promes.cnrs.fr
Christoph LauterAssistant Professor of Computer Science, University of Alaska AnchorageVerified email at alaska.edu
Nicolas BrunieSiFiveVerified email at sifive.com
Mioara JoldesCNRSVerified email at laas.fr
Érik Martin-DorelAssociate Professor in Computer Science, Univ. Toulouse III - Paul SabatierVerified email at irit.fr
François BobotVerified email at bobot.eu
Claude MarchéSenior Research Scientist, InriaVerified email at inria.fr
Iguernlala (Iguernelala) MohamedFunctoriVerified email at functori.com
Jacques-Henri JourdanCNRS, Laboratoire Méthodes FormellesVerified email at cnrs.fr
Xavier LeroyCollège de FranceVerified email at college-de-france.fr
Andrei PaskevichAssociate Professor of Computer Science, Paris-Saclay UniversityVerified email at u-psud.fr

Guillaume Melquiond

Inria, University Paris Saclay

Verified email at inria.fr - Homepage

Computer arithmetic Program verification Formal proofs


Title Sort by citations Sort by year Sort by title	Cited by Cited by	Year
Handbook of floating-point arithmetic JM Muller, N Brisebarre, F De Dinechin, CP Jeannerod, L Vincent, ... Birkhauser, 2009	975*	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	291	2008
Flocq: A unified library for proving floating-point algorithms in Coq S Boldo, G Melquiond 20th IEEE Symposium on Computer Arithmetic, 243-252, 2010	191	2010
Coquelicot: A user-friendly library of real analysis for Coq S Boldo, C Lelay, G Melquiond Mathematics in Computer Science 9, 41-62, 2015	152	2015
Certification of bounds on expressions involving rounded operators M Daumas, G Melquiond Transactions on Mathematical Software 37 (1), 1-20, 2010	148	2010
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	144	2011
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	116	2006
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	107	2013
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	103	2009
The design of the Boost interval arithmetic library H Brönnimann, G Melquiond, S Pion Theoretical Computer Science 351 (1), 111-118, 2006	91	2006
Guaranteed proofs using interval arithmetic M Daumas, G Melquiond, C Munoz 17th IEEE Symposium on Computer Arithmetic, 188-195, 2005	77	2005
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	75	2016
Floating-point arithmetic in the Coq system G Melquiond Information and Computation 216, 14-23, 2012	67	2012
Proving bounds on real-valued functions with computations G Melquiond International Joint Conference on Automated Reasoning, 2-17, 2008	65	2008
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	64	2013
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	64	2008
Verified compilation of floating-point computations S Boldo, JH Jourdan, X Leroy, G Melquiond Journal of Automated Reasoning 54, 135-163, 2015	60	2015
Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System S Boldo, G Melquiond Elsevier, 2017	53	2017
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	51	2012
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	51	2010

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Follow

Cited by

Co-authors