2020

Conference papers

auteur
Guillaume Melquiond, Raphaël Rieu-Helft
titre
WhyMP, a Formally Verified Arbitrary-Precision Integer Library
article
ISSAC 2020: 45th International Symposium on Symbolic and Algebraic Computation, Jul 2020, Kalamata, Greece
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02566654/file/main.pdf BibTex

2019

Journal articles

auteur
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
titre
Formally Verified Approximations of Definite Integrals
article
Journal of Automated Reasoning, Springer Verlag, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01630143/file/main.pdf BibTex

Conference papers

auteur
Guillaume Melquiond
titre
Arithmétique des Ordinateurs et Preuves Formelles
article
JFLA 2019 - 30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02013540/file/article.pdf BibTex
auteur
Guillaume Melquiond, Raphaël Rieu-Helft
titre
Formal Verification of a State-of-the-Art Integer Square Root
article
ARITH-26 2019 - 26th IEEE 26th Symposium on Computer Arithmetic, Jun 2019, Kyoto, Japan. pp.183-186, ⟨10.1109/ARITH.2019.00041⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02092970/file/main.pdf BibTex

Habilitation à diriger des recherches

auteur
Guillaume Melquiond
titre
Formal Verification for Numerical Computations, and the Other Way Around
article
Computer Arithmetic. Université Paris Sud, 2019
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-02194683/file/hdr.pdf BibTex

2018

Conference papers

auteur
Guillaume Melquiond, Raphaël Rieu-Helft
titre
A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms
article
9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.178-193, ⟨10.1007/978-3-319-94205-6_13⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01699754/file/main.pdf BibTex

Books

auteur
Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Serge Torres
titre
Handbook of Floating-point Arithmetic (2nd edition)
article
Birkhäuser Basel, pp.1-627, 2018, 978-3319765259. ⟨10.1007/978-3-319-76526-6⟩
Accès au bibtex
BibTex

2017

Conference papers

auteur
Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex
titre
A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMT
article
29th International Conference on Computer Aided Verification, Jul 2017, Heidelberg, Germany. pp.419-435, ⟨10.1007/978-3-319-63390-9_22⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01522770/file/main.pdf BibTex
auteur
Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond
titre
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library
article
9th Working Conference on Verified Software: Theories, Tools, and Experiments, Jul 2017, Heidelberg, Germany. pp.84-101, ⟨10.1007/978-3-319-72308-2_6⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01519732/file/main.pdf BibTex

Books

auteur
Sylvie Boldo, Guillaume Melquiond
titre
Computer Arithmetic and Formal Proofs
article
ISTE Press - Elsevier, pp.326, 2017, 9781785481123
Accès au bibtex
BibTex

2016

Journal articles

auteur
Érik Martin-Dorel, Guillaume Melquiond
titre
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
article
Journal of Automated Reasoning, Springer Verlag, 2016, 57 (3), pp.187-217. ⟨10.1007/s10817-015-9350-4⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01086460/file/article.pdf BibTex
auteur
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
titre
Formalization of Real Analysis: A Survey of Proof Assistants and Libraries
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2016, 26 (7), pp.1196-1233. ⟨10.1017/S0960129514000437⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00806920/file/article.pdf BibTex

Conference papers

auteur
Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
titre
Formally Verified Approximations of Definite Integrals
article
Interactive Theorem Proving, Aug 2016, Nancy, France. ⟨10.1007/978-3-319-43144-4_17⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01289616/file/main.pdf BibTex

2015

Journal articles

auteur
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
titre
Verified Compilation of Floating-Point Computations
article
Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00862689/file/floating-point-compcert.pdf BibTex
auteur
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
titre
Coquelicot: A User-Friendly Library of Real Analysis for Coq
article
Mathematics in Computer Science, Springer, 2015, 9 (1), pp.41-62. ⟨10.1007/s11786-014-0181-1⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00860648/file/article.pdf BibTex

2014

Journal articles

auteur
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
titre
Trusting computations: a mechanized proof from partial differential equations to actual program
article
Computers and Mathematics with Applications, Elsevier, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00769201/file/RR-8197.pdf BibTex

Conference papers

auteur
Guillaume Melquiond
titre
Automating the verification of floating-point algorithms
article
12th International Workshop on Satisfiability Modulo Theories, Jul 2014, Wien, Austria
Accès au bibtex
BibTex

2013

Journal articles

auteur
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
titre
Wave equation numerical resolution: a comprehensive mechanized proof of a C program
article
Journal of Automated Reasoning, Springer Verlag, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00649240/file/RR-7826.pdf BibTex
auteur
Érik Martin-Dorel, Guillaume Melquiond, Jean-Michel Muller
titre
Some issues related to double roundings
article
BIT Numerical Mathematics, Springer Verlag, 2013, 53 (4), pp.897-924. ⟨10.1007/s10543-013-0436-2⟩
Accès au texte intégral et bibtex
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00644408/file/Version_Finale_DoubleRoundings.pdf BibTex
auteur
Guillaume Melquiond, W. Georg Nowak, Paul Zimmermann
titre
Numerical Approximation of the Masser-Gramain Constant to Four Decimal Digits: delta=1.819...
article
Mathematics of Computation, American Mathematical Society, 2013, 82, pp.1235-1246. ⟨10.1090/S0025-5718-2012-02635-4⟩
Accès au bibtex
BibTex

Conference papers

auteur
Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
titre
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
article
Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00743090/file/article.pdf BibTex
auteur
Daisuke Ishii, Guillaume Melquiond, Shin Nakajima
titre
Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus
article
iFM - 10th International Conference on Integrated Formal Methods - 2013, Jun 2013, Turku, Finland. pp.139-153, ⟨10.1007/978-3-642-38613-8_10⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00806701/file/article.pdf BibTex
auteur
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
titre
Preserving User Proofs Across Specification Changes
article
Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00875395/file/main.pdf BibTex
auteur
Guillaume Melquiond
titre
Automations for verifying floating-point algorithms
article
5th Coq Workshop, Jul 2013, Rennes, France
Accès au bibtex
BibTex

Book sections

auteur
Sylvie Boldo, Guillaume Melquiond
titre
Arithmétique des ordinateurs et preuves formelles
article
Informatique mathématique : Une photographie en 2013, 2013
Accès au bibtex
BibTex

Other publications

auteur
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich
titre
The Why3 platform 0.81
article
2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00822856/file/manual-0.81.pdf BibTex

2012

Journal articles

auteur
Guillaume Melquiond
titre
Floating-point arithmetic in the Coq system
article
Information and Computation, Elsevier, 2012, 216, pp.14-23. ⟨10.1016/j.ic.2011.09.005⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00797913/file/article.pdf BibTex

Conference papers

auteur
Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala
titre
Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers
article
10th International Workshop on Satisfiability Modulo Theories, Jun 2012, Manchester, United Kingdom. pp.12-21
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01785166/file/article.pdf BibTex
auteur
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond
titre
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
article
6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. pp.67-81, ⟨10.1007/978-3-642-31365-3_8⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00687640/file/main.pdf BibTex
auteur
Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
titre
Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives
article
CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. pp.289-304, ⟨10.1007/978-3-642-35308-6_22⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00712938/file/article.pdf BibTex
auteur
Catherine Lelay, Guillaume Melquiond
titre
Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert
article
JFLA - Journées Francophone des Langages Applicatifs - 2012, Feb 2012, Carnac, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00642206/file/lelay.pdf BibTex
auteur
Sylvie Boldo, Guillaume Melquiond
titre
Arithmétique des ordinateurs et preuves formelles
article
École des Jeunes Chercheurs en Informatique Mathématique, GDR Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00755333/file/main.pdf BibTex

2011

Journal articles

auteur
Florent de Dinechin, Christoph Lauter, Guillaume Melquiond
titre
Certifying the floating-point implementation of an elementary function using Gappa
article
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2011, 60 (2), pp.242-253. ⟨10.1109/TC.2010.128⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/ensl-00200830/file/10-tc.pdf BibTex

Conference papers

auteur
Sylvie Boldo, Guillaume Melquiond
titre
Flocq: A Unified Library for Proving Floating-point Algorithms in Coq
article
Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Jul 2011, Tübingen, Germany. pp.243-252, ⟨10.1109/ARITH.2011.40⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00534854/file/11-arith20-article.pdf BibTex

2010

Journal articles

auteur
Marc Daumas, Guillaume Melquiond
titre
Certification of bounds on expressions involving rounded operators
article
ACM Transactions on Mathematical Software, Association for Computing Machinery, 2010, 37 (1), pp.1-20. ⟨10.1145/1644001.1644002⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00127769/file/article.pdf BibTex

Conference papers

auteur
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
titre
Formal proof of a wave equation resolution scheme: the method error
article
ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. pp.147-162, ⟨10.1007/978-3-642-14052-5_12⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00450789/file/RR-7181.pdf BibTex

Books

auteur
Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, Serge Torres
titre
Handbook of Floating-Point Arithmetic
article
Birkhauser Boston, pp.572, 2010
Accès au bibtex
BibTex

2009

Journal articles

auteur
Siegfried Rump, Paul Zimmermann, Sylvie Boldo, Guillaume Melquiond
titre
Computing predecessor and successor in rounding to nearest
article
BIT Numerical Mathematics, Springer Verlag, 2009, 49 (2), pp.419-431. ⟨10.1007/s10543-009-0218-z⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00337537/file/RuZiBoMe08.pdf BibTex

Conference papers

auteur
Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
titre
Combining Coq and Gappa for Certifying Floating-Point Programs
article
16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Jul 2009, Grand Bend, Ontario, Canada. pp.59-74, ⟨10.1007/978-3-642-02614-0_10⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00432726/file/09-calculemus-article.pdf BibTex

2008

Journal articles

auteur
Sylvie Boldo, Guillaume Melquiond
titre
Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd
article
IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2008, 57 (4), pp.462-471. ⟨10.1109/TC.2007.70819⟩
Accès au texte intégral et bibtex
https://hal-ens-lyon.archives-ouvertes.fr/inria-00080427/file/odd-rounding.pdf BibTex

Conference papers

auteur
Guillaume Melquiond
titre
Floating-point arithmetic in the Coq system
article
8th Conference on Real Numbers and Computers, Jul 2008, Santiago de Compostela, Spain. pp.93-102
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01780385/file/08-rnc8-article.pdf BibTex
auteur
Guillaume Melquiond
titre
Proving bounds on real-valued functions with computations
article
International Joint Conference on Automated Reasoning, IJCAR 2008, Aug 2008, Sydney, Australia. pp.2--17, ⟨10.1007/978-3-540-71070-7_2⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00180138/file/article.pdf BibTex

Reports

auteur
Guillaume Melquiond, Sylvain Pion
titre
Directed Rounding Arithmetic Operations in C++
article
[Research Report] RR-6757, INRIA. 2008, pp.11
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00345094/file/RR-6757.pdf BibTex

2007

Journal articles

auteur
Guillaume Melquiond, Sylvain Pion
titre
Formally Certified Floating-Point Filters For Homogeneous Geometric Predicates
article
RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2007, 41, pp.57-69. ⟨10.1051/ita:2007005⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071232/file/pion_melquiond.pdf BibTex

2006

Journal articles

auteur
Hervé Brönnimann, Guillaume Melquiond, Sylvain Pion
titre
The design of the Boost interval arithmetic library
article
Theoretical Computer Science, Elsevier, 2006, Real Numbers and Computers, 351 (1), pp.111-118. ⟨10.1016/j.tcs.2005.09.062⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00344412/file/tcs.pdf BibTex

Reports

auteur
Sylvain Pion, Guillaume Melquiond, Hervé Brönnimann
titre
A proposal for the C++ standard : Bool_set, multi-valued logic
article
[Research Report] RR-5967, INRIA. 2006, pp.22
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00089230/file/RR-5967.pdf BibTex
auteur
Hervé Brönnimann, Guillaume Melquiond, Sylvain Pion
titre
A Proposal to add Interval Arithmetic to the C++ Standard Library
article
[Research Report] RR-5646, INRIA. 2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071231/file/RR-5646.pdf BibTex

Theses

auteur
Guillaume Melquiond
titre
De l'arithmétique d'intervalles à la certification de programmes
article
Arithmétique des ordinateurs. École Normale Supérieure de Lyon, 2006. Français. ⟨NNT : 2006ENSL0388⟩
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01094485/file/06-these.pdf BibTex

2005

Conference papers

auteur
Sylvie Boldo, Guillaume Melquiond
titre
When double rounding is odd
article
17th IMACS World Congress, Jul 2005, Paris, France. pp.11
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070603/file/BolMel.pdf BibTex
auteur
Guillaume Melquiond, Sylvain Pion
titre
Formal certification of arithmetic filters for geometric predicates
article
17th IMACS World Congress, 2005, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00344518/file/IMACS_05_FPgeo.pdf BibTex
auteur
Marc Daumas, Guillaume Melquiond, César Muñoz
titre
Guaranteed Proofs Using Interval Arithmetic
article
17th IEEE Symposium on Computer Arithmetic, 2005, Cape Cod, Massachusetts, United States. pp.188-195, ⟨10.1109/ARITH.2005.25⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00164621/file/Daumas_Melquiond_et_Munoz.pdf BibTex

Reports

auteur
Florent de Dinechin, Christoph Lauter, Guillaume Melquiond
titre
Assisted verification of elementary functions
article
RR-5683, INRIA. 2005, pp.17
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070330/file/RR-5683.pdf BibTex

2004

Conference papers

auteur
Marc Daumas, Guillaume Melquiond
titre
Generating formally certified bounds on values and round-off errors
article
Real Numbers and Computers, 2004, Dagstuhl, Germany. pp.55-70
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00070739/file/RR-5259.pdf BibTex

2003

Conference papers

auteur
Hervé Brönnimann, Guillaume Melquiond, Sylvain Pion
titre
The Boost Interval Arithmetic Library
article
Real Numbers and Computers, 2003, Lyon, France. pp.65-80
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00348711/file/rnc.pdf BibTex