| Handbook of floating-point arithmetic JM Muller, N Brisebarre, F De Dinechin, CP Jeannerod, L Vincent, ... Birkhauser, 2009 | 966* | 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 | 287 | 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 | 189 | 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 | 147 | 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 | 143 | 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 | 106 | 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 | 74 | 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 | 64 | 2008 |
| 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 |
| 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 | 63 | 2013 |
| Verified compilation of floating-point computations S Boldo, JH Jourdan, X Leroy, G Melquiond Journal of Automated Reasoning 54, 135-163, 2015 | 59 | 2015 |
| Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System S Boldo, G Melquiond Elsevier, 2017 | 52 | 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 | 52 | 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 |
Florent de Dinechinprofessor, INSA-Lyon在 insa-lyon.fr 的电子邮件经过验证
