Skip to Main content

Keywords

Number of documents

62

Guillaume Melquiond's Publications


Brought to you by HAL.


Journal articles16 documents

  • Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Journal of Automated Reasoning, Springer Verlag, 2019, 62 (2), pp.281-300. ⟨10.1007/s10817-018-9463-7⟩. ⟨hal-01630143v2⟩
  • Érik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. Journal of Automated Reasoning, Springer Verlag, 2016, 57 (3), pp.187-217. ⟨10.1007/s10817-015-9350-4⟩. ⟨hal-01086460v2⟩
  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Formalization of Real Analysis: A Survey of Proof Assistants and Libraries. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2016, 26 (7), pp.1196-1233. ⟨10.1017/S0960129514000437⟩. ⟨hal-00806920v2⟩
  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Coquelicot: A User-Friendly Library of Real Analysis for Coq. Mathematics in Computer Science, Springer, 2015, 9 (1), pp.41-62. ⟨10.1007/s11786-014-0181-1⟩. ⟨hal-00860648v2⟩
  • Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩. ⟨hal-00862689v3⟩
  • Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Trusting computations: a mechanized proof from partial differential equations to actual program. Computers & Mathematics with Applications, Elsevier, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩. ⟨hal-00769201v3⟩
  • Guillaume Melquiond, Werner Georg Nowak, Paul Zimmermann. Numerical Approximation of the Masser-Gramain Constant to Four Decimal Digits: delta=1.819.... Mathematics of Computation, American Mathematical Society, 2013, 82, pp.1235-1246. ⟨10.1090/S0025-5718-2012-02635-4⟩. ⟨hal-00644166⟩
  • Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, Springer Verlag, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩. ⟨hal-00649240v3⟩
  • Érik Martin-Dorel, Guillaume Melquiond, Jean-Michel Muller. Some issues related to double roundings. BIT Numerical Mathematics, Springer Verlag, 2013, 53 (4), pp.897-924. ⟨10.1007/s10543-013-0436-2⟩. ⟨ensl-00644408v3⟩
  • Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, Elsevier, 2012, 216, pp.14-23. ⟨10.1016/j.ic.2011.09.005⟩. ⟨hal-00797913⟩
  • Florent de Dinechin, Christoph Lauter, Guillaume Melquiond. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2011, 60 (2), pp.242-253. ⟨10.1109/TC.2010.128⟩. ⟨ensl-00200830v2⟩
  • Marc Daumas, Guillaume Melquiond. Certification of bounds on expressions involving rounded operators. ACM Transactions on Mathematical Software, Association for Computing Machinery, 2010, 37 (1), pp.1-20. ⟨10.1145/1644001.1644002⟩. ⟨hal-00127769v3⟩
  • Siegfried Rump, Paul Zimmermann, Sylvie Boldo, Guillaume Melquiond. Computing predecessor and successor in rounding to nearest. BIT Numerical Mathematics, Springer Verlag, 2009, 49 (2), pp.419-431. ⟨10.1007/s10543-009-0218-z⟩. ⟨inria-00337537⟩
  • Sylvie Boldo, Guillaume Melquiond. Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd. IEEE Transactions on Computers, Institute of Electrical and Electronics Engineers, 2008, 57 (4), pp.462-471. ⟨10.1109/TC.2007.70819⟩. ⟨inria-00080427v2⟩
  • Guillaume Melquiond, Sylvain Pion. Formally Certified Floating-Point Filters For Homogeneous Geometric Predicates. RAIRO - Theoretical Informatics and Applications (RAIRO: ITA), EDP Sciences, 2007, 41, pp.57-69. ⟨10.1051/ita:2007005⟩. ⟨inria-00071232v2⟩
  • Hervé Brönnimann, Guillaume Melquiond, Sylvain Pion. The design of the Boost interval arithmetic library. Theoretical Computer Science, Elsevier, 2006, Real Numbers and Computers, 351 (1), pp.111-118. ⟨10.1016/j.tcs.2005.09.062⟩. ⟨inria-00344412⟩

Conference papers32 documents

  • Guillaume Melquiond. Plotting in a Formally Verified Way. Proceedings of the 6th Workshop on Formal Integrated Development Environment, May 2021, Online, United States. pp.39-45, ⟨10.4204/EPTCS.338.6⟩. ⟨hal-03168208v2⟩
  • Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond. A strong call-by-need calculus. Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires, Argentina. pp.1-22, ⟨10.4230/LIPIcs.FSCD.2021.9⟩. ⟨hal-03149692v2⟩
  • Sylvie Boldo, Guillaume Melquiond. Some Formal Tools for Computer Arithmetic: Flocq and Gappa. 28th IEEE International Symposium on Computer Arithmetic, Jun 2021, Online, Italy. ⟨hal-03233227⟩
  • Guillaume Melquiond, Raphaël Rieu-Helft. WhyMP, a Formally Verified Arbitrary-Precision Integer Library. ISSAC 2020 - 45th International Symposium on Symbolic and Algebraic Computation, Jul 2020, Kalamata, Greece. pp.352-359, ⟨10.1145/3373207.3404029⟩. ⟨hal-02566654v2⟩
  • Guillaume Melquiond, Raphaël Rieu-Helft. Formal Verification of a State-of-the-Art Integer Square Root. ARITH-26 2019 - 26th IEEE 26th Symposium on Computer Arithmetic, Jun 2019, Kyoto, Japan. pp.183-186, ⟨10.1109/ARITH.2019.00041⟩. ⟨hal-02092970⟩
  • Guillaume Melquiond. Arithmétique des Ordinateurs et Preuves Formelles. JFLA 2019 - 30èmes Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France. ⟨hal-02013540⟩
  • Guillaume Melquiond, Raphaël Rieu-Helft. A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms. 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.178-193, ⟨10.1007/978-3-319-94205-6_13⟩. ⟨hal-01699754v2⟩
  • Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond. How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. 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⟩. ⟨hal-01519732v2⟩
  • Sylvain Conchon, Mohamed Iguernelala, Kailiang Ji, Guillaume Melquiond, Clément Fumex. A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMT. 29th International Conference on Computer Aided Verification, Jul 2017, Heidelberg, Germany. pp.419-435, ⟨10.1007/978-3-319-63390-9_22⟩. ⟨hal-01522770⟩
  • Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Interactive Theorem Proving, Aug 2016, Nancy, France. ⟨10.1007/978-3-319-43144-4_17⟩. ⟨hal-01289616v2⟩
  • Érik Martin-Dorel, Guillaume Melquiond. CoqInterval: A Toolbox for Proving Non-linear Univariate Inequalities in Coq. MAP 2016 conference on Effective Analysis: Foundations, Implementations, Certification, Jan 2016, Marseille, France. ⟨hal-03155045⟩
  • Érik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq (Journées FAC 2016). 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. ⟨hal-03176418⟩
  • Guillaume Melquiond. Automating the verification of floating-point algorithms. 12th International Workshop on Satisfiability Modulo Theories, Jul 2014, Wien, Austria. ⟨hal-01110669⟩
  • François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. Preserving User Proofs Across Specification Changes. Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. pp.191-201. ⟨hal-00875395⟩
  • Guillaume Melquiond. Automations for verifying floating-point algorithms. 5th Coq Workshop, Jul 2013, Rennes, France. ⟨hal-01110666⟩
  • Daisuke Ishii, Guillaume Melquiond, Shin Nakajima. Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. iFM - 10th International Conference on Integrated Formal Methods - 2013, Jun 2013, Turku, Finland. pp.139-153, ⟨10.1007/978-3-642-38613-8_10⟩. ⟨hal-00806701⟩
  • Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115. ⟨hal-00743090v2⟩
  • Sylvie Boldo, Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. École des Jeunes Chercheurs en Informatique Mathématique, GDR Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30. ⟨hal-00755333⟩
  • François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, et al.. A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. pp.67-81, ⟨10.1007/978-3-642-31365-3_8⟩. ⟨hal-00687640v2⟩
  • Sylvain Conchon, Guillaume Melquiond, Cody Roux, Mohamed Iguernelala. Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. 10th International Workshop on Satisfiability Modulo Theories, Jun 2012, Manchester, United Kingdom. pp.12-21. ⟨hal-01785166⟩
  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives. 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⟩. ⟨hal-00712938v2⟩
  • Catherine Lelay, Guillaume Melquiond. Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert. JFLA - Journées Francophone des Langages Applicatifs - 2012, Feb 2012, Carnac, France. ⟨hal-00642206v2⟩
  • Sylvie Boldo, Guillaume Melquiond. Flocq: A Unified Library for Proving Floating-point Algorithms in Coq. Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Jul 2011, Tübingen, Germany. pp.243-252, ⟨10.1109/ARITH.2011.40⟩. ⟨inria-00534854v2⟩
  • Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, et al.. Formal proof of a wave equation resolution scheme: the method error. ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. pp.147-162, ⟨10.1007/978-3-642-14052-5_12⟩. ⟨inria-00450789v3⟩
  • Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. 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⟩. ⟨inria-00432726⟩
  • Guillaume Melquiond. Floating-point arithmetic in the Coq system. 8th Conference on Real Numbers and Computers, Jul 2008, Santiago de Compostela, Spain. pp.93-102. ⟨hal-01780385⟩
  • Guillaume Melquiond. Proving bounds on real-valued functions with computations. International Joint Conference on Automated Reasoning, IJCAR 2008, Aug 2008, Sydney, Australia. pp.2--17, ⟨10.1007/978-3-540-71070-7_2⟩. ⟨hal-00180138⟩
  • Guillaume Melquiond, Sylvain Pion. Formal certification of arithmetic filters for geometric predicates. 17th IMACS World Congress, 2005, Paris, France. ⟨inria-00344518⟩
  • Sylvie Boldo, Guillaume Melquiond. When double rounding is odd. 17th IMACS World Congress, Jul 2005, Paris, France. pp.11. ⟨inria-00070603v2⟩
  • Marc Daumas, Guillaume Melquiond, César Muñoz. Guaranteed Proofs Using Interval Arithmetic. 17th IEEE Symposium on Computer Arithmetic, 2005, Cape Cod, Massachusetts, United States. pp.188-195, ⟨10.1109/ARITH.2005.25⟩. ⟨hal-00164621⟩
  • Marc Daumas, Guillaume Melquiond. Generating formally certified bounds on values and round-off errors. Real Numbers and Computers, 2004, Dagstuhl, Germany. pp.55-70. ⟨inria-00070739⟩
  • Hervé Brönnimann, Guillaume Melquiond, Sylvain Pion. The Boost Interval Arithmetic Library. Real Numbers and Computers, 2003, Lyon, France. pp.65-80. ⟨inria-00348711⟩

Books3 documents

  • Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, et al.. Handbook of Floating-point Arithmetic (2nd edition). Birkhäuser Basel, pp.1-627, 2018, 978-3319765259. ⟨10.1007/978-3-319-76526-6⟩. ⟨hal-01766584⟩
  • Sylvie Boldo, Guillaume Melquiond. Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. ISTE Press - Elsevier, pp.326, 2017, 9781785481123. ⟨hal-01632617⟩
  • Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, et al.. Handbook of Floating-Point Arithmetic. Birkhauser Boston, pp.572, 2010. ⟨ensl-00379167⟩

Book sections1 document

  • Sylvie Boldo, Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. Informatique mathématique : Une photographie en 2013, 2013. ⟨hal-01767900⟩

Patents1 document

  • Jean-Christophe Filliâtre, Andrei Paskevich, Guillaume Melquiond, Claude Marché, François Bobot. Why3 version 1.0. France, N° de brevet: IDDN.FR.001.420003.000.S.P.2019.000.20600. 2018. ⟨hal-03136256⟩

Other publications1 document

  • François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. The Why3 platform 0.81. 2013. ⟨hal-00822856⟩

Preprints, Working Papers, ...1 document

  • Guillaume Melquiond, Raphaël Rieu-Helft. WhyMP, a Formally Verified Arbitrary-Precision Integer Library. 2020. ⟨hal-03233220⟩

Reports5 documents

  • Érik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions in Coq. [Research Report] IRIT-RR-2014-09-FR, IRIT : Institut de Recherche Informatique de Toulouse. 2014, pp.1-32. ⟨hal-03260617⟩
  • Guillaume Melquiond, Sylvain Pion. Directed Rounding Arithmetic Operations in C++. [Research Report] RR-6757, INRIA. 2008, pp.11. ⟨inria-00345094⟩
  • Hervé Brönnimann, Guillaume Melquiond, Sylvain Pion. A Proposal to add Interval Arithmetic to the C++ Standard Library. [Research Report] RR-5646, INRIA. 2006. ⟨inria-00071231⟩
  • Sylvain Pion, Guillaume Melquiond, Hervé Brönnimann. A proposal for the C++ standard : Bool_set, multi-valued logic. [Research Report] RR-5967, INRIA. 2006, pp.22. ⟨inria-00089230v2⟩
  • Florent de Dinechin, Christoph Lauter, Guillaume Melquiond. Assisted verification of elementary functions. RR-5683, INRIA. 2005, pp.17. ⟨inria-00070330⟩

Theses1 document

  • Guillaume Melquiond. De l'arithmétique d'intervalles à la certification de programmes. Arithmétique des ordinateurs. École Normale Supérieure de Lyon, 2006. Français. ⟨NNT : 2006ENSL0388⟩. ⟨tel-01094485⟩

Habilitation à diriger des recherches1 document

  • Guillaume Melquiond. Formal Verification for Numerical Computations, and the Other Way Around. Computer Arithmetic. Université Paris Sud, 2019. ⟨tel-02194683⟩