Παρακολούθηση
Guillaume Melquiond
Guillaume Melquiond
Inria, University Paris Saclay
Η διεύθυνση ηλεκτρονικού ταχυδρομείου έχει επαληθευτεί στον τομέα inria.fr - Αρχική σελίδα
Τίτλος
Παρατίθεται από
Παρατίθεται από
Έτος
Handbook of floating-point arithmetic
JM Muller, N Brisebarre, F De Dinechin, CP Jeannerod, L Vincent, ...
Birkhauser, 2009
849*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
2672008
Flocq: A unified library for proving floating-point algorithms in Coq
S Boldo, G Melquiond
20th IEEE Symposium on Computer Arithmetic, 243-252, 2010
1732010
Coquelicot: A user-friendly library of real analysis for Coq
S Boldo, C Lelay, G Melquiond
Mathematics in Computer Science 9 (1), 41-62, 2015
1322015
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
1302011
Certification of bounds on expressions involving rounded operators
M Daumas, G Melquiond
Transactions on Mathematical Software 37 (1), 1-20, 2010
1302010
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
1112006
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
982009
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
942013
The design of the Boost interval arithmetic library
H Brönnimann, G Melquiond, S Pion
Theoretical Computer Science 351 (1), 111-118, 2006
872006
Guaranteed proofs using interval arithmetic
M Daumas, G Melquiond, C Munoz
17th IEEE Symposium on Computer Arithmetic, 188-195, 2005
772005
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
682016
Proving bounds on real-valued functions with computations
G Melquiond
International Joint Conference on Automated Reasoning, 2-17, 2008
642008
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
642008
Verified Compilation of Floating-Point Computations
S Boldo, JH Jourdan, X Leroy, G Melquiond
Journal of Automated Reasoning 54 (2), 135-163, 2015
582015
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
582013
Floating-point arithmetic in the Coq system
G Melquiond
Information and Computation 216, 14-23, 2012
472012
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
472010
De l’arithmétique d’intervalles à la certification de programmes
G Melquiond
PhD thesis, ÉNS Lyon, France, 2006
462006
Formally certified floating-point filters for homogeneous geometric predicates
G Melquiond, S Pion
RAIRO-Theoretical Informatics and Applications 41 (01), 57-69, 2007
442007
Δεν είναι δυνατή η εκτέλεση της ενέργειας από το σύστημα αυτή τη στιγμή. Προσπαθήστε ξανά αργότερα.
Άρθρα 1–20