2024
Preprints, Working Papers, ...
- auteur
- Florian Faissole, Paul Geneau de Lamarlière, Guillaume Melquiond
- titre
- End-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation
- article
- 2024
- Accès au texte intégral et bibtex
-
2023
Journal articles
- auteur
- Guillaume Melquiond, Raphaël Rieu-Helft
- titre
- WhyMP, a Formally Verified Arbitrary-Precision Integer Library
- article
- Journal of Symbolic Computation, 2023, 115, pp.74-95. ⟨10.1016/j.jsc.2022.07.007⟩
- Accès au texte intégral et bibtex
-
- auteur
- Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
- titre
- A strong call-by-need calculus
- article
- Logical Methods in Computer Science, 2023, 19 (1), pp.39. ⟨10.46298/lmcs-19(1:21)2023⟩
- Accès au texte intégral et bibtex
-
- auteur
- Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller
- titre
- Floating-point arithmetic
- article
- Acta Numerica, 2023, 32, pp.203-290. ⟨10.1017/S0962492922000101⟩
- Accès au texte intégral et bibtex
-
- auteur
- Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux
- titre
- Enabling Floating-Point Arithmetic in the Coq Proof Assistant
- article
- Journal of Automated Reasoning, 2023, 67 (33), ⟨10.1007/s10817-023-09679-x⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Paul Geneau de Lamarlière, Guillaume Melquiond, Florian Faissole
- titre
- Slimmer Formal Proofs for Mathematical Libraries
- article
- 30th IEEE International Symposium on Computer Arithmetic, Sep 2023, Portland (Oregon), United States. pp.4
- Accès au texte intégral et bibtex
-
- auteur
- Assia Mahboubi, Guillaume Melquiond
- titre
- Manifest Termination
- article
- TYPES 2023 - 29th International Conference on Types for Proofs and Programs, Jun 2023, Valencia, Spain. pp.1-3
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- auteur
- Josué Moreau, Guillaume Melquiond
- titre
- A Safe Low-level Language for Computer Algebra and its Formally Verified Compiler
- article
- 2023
- Accès au texte intégral et bibtex
-
2021
Conference papers
- auteur
- Guillaume Melquiond
- titre
- Plotting in a Formally Verified Way
- article
- Proceedings of the 6th Workshop on Formal Integrated Development Environment, May 2021, Online, United States. pp.39-45, ⟨10.4204/EPTCS.338.6⟩
- Accès au texte intégral et bibtex
-
- auteur
- Sylvie Boldo, Guillaume Melquiond
- titre
- Some Formal Tools for Computer Arithmetic: Flocq and Gappa
- article
- ARITH 2021 - 28th IEEE International Symposium on Computer Arithmetic, Jun 2021, Online, Italy
- Accès au texte intégral et bibtex
-
- auteur
- Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
- titre
- A strong call-by-need calculus
- article
- FSCD 2021 - 6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires, Argentina. pp.1-22, ⟨10.4230/LIPIcs.FSCD.2021.9⟩
- Accès au texte intégral et bibtex
-
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. pp.352-359, ⟨10.1145/3373207.3404029⟩
- Accès au texte intégral et bibtex
-
2019
Journal articles
- auteur
- Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote
- titre
- Formally Verified Approximations of Definite Integrals
- article
- Journal of Automated Reasoning, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩
- Accès au texte intégral et 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
-
- 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
-
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
-
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
-
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
-
Patents
- auteur
- Jean-Christophe Filliâtre, Andrei Paskevich, Guillaume Melquiond, Claude Marché, François Bobot
- titre
- Why3 version 1.0
- article
- France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018
- Accès au bibtex
-
2017
Conference papers
- 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
-
- 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
-
Books
- auteur
- Sylvie Boldo, Guillaume Melquiond
- titre
- Computer Arithmetic and Formal Proofs
- article
- ISTE Press - Elsevier, pp.326, 2017, 9781785481123
- Accès au bibtex
-
2016
Journal articles
- 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, 2016, 26 (7), pp.1196-1233. ⟨10.1017/S0960129514000437⟩
- Accès au texte intégral et bibtex
-
- auteur
- Érik Martin-Dorel, Guillaume Melquiond
- titre
- Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
- article
- Journal of Automated Reasoning, 2016, 57 (3), pp.187-217. ⟨10.1007/s10817-015-9350-4⟩
- Accès au texte intégral et bibtex
-
Conference papers
- auteur
- Érik Martin-Dorel, Guillaume Melquiond
- titre
- Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq (Journées FAC 2016)
- article
- Journées Formalisation des Activités Concurrentes (FAC 2016), Groupe IFSE du RTRA STAE (Réseau Thématique de Recherche Avancée « Sciences et Technologies pour l’Aéronautique et l’Espace » de Toulouse), Mar 2016, Toulouse, France
- Accès au bibtex
-
- 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
-
- auteur
- Érik Martin-Dorel, Guillaume Melquiond
- titre
- CoqInterval: A Toolbox for Proving Non-linear Univariate Inequalities in Coq
- article
- MAP 2016 conference on Effective Analysis: Foundations, Implementations, Certification, Jan 2016, Marseille, France
- Accès au 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, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩
- Accès au texte intégral et bibtex
-
- auteur
- Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
- titre
- Coquelicot: A User-Friendly Library of Real Analysis for Coq
- article
- Mathematics in Computer Science, 2015, 9 (1), pp.41-62. ⟨10.1007/s11786-014-0181-1⟩
- Accès au texte intégral et 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 & Mathematics with Applications, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩
- Accès au texte intégral et 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
-
Reports
- auteur
- Érik Martin-Dorel, Guillaume Melquiond
- titre
- Proving Tight Bounds on Univariate Expressions in Coq
- article
- [Research Report] IRIT-RR-2014-09-FR, IRIT : Institut de Recherche Informatique de Toulouse. 2014, pp.1-32
- Accès au bibtex
-
2013
Journal articles
- auteur
- Érik Martin-Dorel, Guillaume Melquiond, Jean-Michel Muller
- titre
- Some issues related to double roundings
- article
- BIT Numerical Mathematics, 2013, 53 (4), pp.897-924. ⟨10.1007/s10543-013-0436-2⟩
- Accès au texte intégral et bibtex
-
- 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, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩
- Accès au texte intégral et bibtex
-
- auteur
- Guillaume Melquiond, Werner Georg Nowak, Paul Zimmermann
- titre
- Numerical Approximation of the Masser-Gramain Constant to Four Decimal Digits: delta=1.819...
- article
- Mathematics of Computation, 2013, 82, pp.1235-1246. ⟨10.1090/S0025-5718-2012-02635-4⟩
- Accès au bibtex
-
Conference papers
- auteur
- Guillaume Melquiond
- titre
- Automations for verifying floating-point algorithms
- article
- 5th Coq Workshop, Jul 2013, Rennes, France
- Accès au bibtex
-
- 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
-
- 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
-
- 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
-
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
-
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
-
2012
Journal articles
- auteur
- Guillaume Melquiond
- titre
- Floating-point arithmetic in the Coq system
- article
- Information and Computation, 2012, 216, pp.14-23. ⟨10.1016/j.ic.2011.09.005⟩
- Accès au texte intégral et bibtex
-
Conference papers
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
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, 2011, 60 (2), pp.242-253. ⟨10.1109/TC.2010.128⟩
- Accès au texte intégral et 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
-
2010
Journal articles
- auteur
- Marc Daumas, Guillaume Melquiond
- titre
- Certification of bounds on expressions involving rounded operators
- article
- ACM Transactions on Mathematical Software, 2010, 37 (1), pp.1-20. ⟨10.1145/1644001.1644002⟩
- Accès au texte intégral et 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
-
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
-
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, 2009, 49 (2), pp.419-431. ⟨10.1007/s10543-009-0218-z⟩
- Accès au texte intégral et 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
-
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, 2008, 57 (4), pp.462-471. ⟨10.1109/TC.2007.70819⟩
- Accès au texte intégral et 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
-
- 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
-
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
-
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), 2007, 41, pp.57-69. ⟨10.1051/ita:2007005⟩
- Accès au texte intégral et 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, 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
-
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
-
- 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
-
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
-
2005
Conference papers
- 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
-
- 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
-
- 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
-
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
-
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
-
Reports
- auteur
- Marc Daumas, Guillaume Melquiond
- titre
- Generating formally certified bounds on values and round-off errors.
- article
- [Research Report] LIP RR-2004-36, Laboratoire de l'informatique du parallélisme. 2004, 2+24p
- Accès au texte intégral et bibtex
-
- auteur
- Sylvie Boldo, Guillaume Melquiond
- titre
- When double rounding is odd
- article
- [Research Report] LIP RR-2004-48, Laboratoire de l'informatique du parallélisme. 2004, 2+7p
- Accès au texte intégral et 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
-