Mots-clés

Nombre de documents

45

Guillaume Melquiond's Publications


Brought to you by HAL.


Article dans une revue15 documents

  • É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 and Mathematics with Applications, Elsevier, 2014, 68 (3), pp.28. 〈10.1016/j.camwa.2014.06.004 〉. 〈hal-00769201v3〉
  • É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〉
  • 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〉
  • Guillaume Melquiond, W. 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〉
  • 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. Journal of Theoretical Computer Science (TCS), Elsevier, 2006, Real Numbers and Computers, 351 (1), pp.111-118. 〈10.1016/j.tcs.2005.09.062〉. 〈inria-00344412〉

Communication dans un congrès21 documents

  • Sylvain Conchon, Mohamed Iguernlala, Kailiang Ji, Guillaume Melquiond, Clément Fumex. A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMT. Viktor Kuncak; Rupak Majumdar. 29th International Conference on Computer Aided Verification, Jul 2017, Heidelberg, Germany. Springer, 10427, pp.419-435, 2017, Lecture Notes in Computer Science. 〈http://cavconference.org/2017/〉. 〈10.1007/978-3-319-63390-9_22〉. 〈hal-01522770〉
  • 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. 10712, 2017, Lecture Notes in Computer Science. 〈https://vstte17.lri.fr/〉. 〈hal-01519732v2〉
  • Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Jasmin Christian Blanchette; Stephan Merz. Interactive Theorem Proving, Aug 2016, Nancy, France. 9807, 2016, Lecture Notes in Computer Science. 〈https://itp2016.inria.fr/〉. 〈10.1007/978-3-319-43144-4_17〉. 〈hal-01289616v2〉
  • Guillaume Melquiond. Automating the verification of floating-point algorithms. 12th International Workshop on Satisfiability Modulo Theories, Jul 2014, Wien, Austria. 〈hal-01110669〉
  • Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond. A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. Alberto Nannarelli and Peter-Michael Seidel and Ping Tak Peter Tang. Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. IEEE, pp.107-115, 2013. 〈hal-00743090v2〉
  • François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. Preserving User Proofs Across Specification Changes. Ernie Cohen and Andrey Rybalchenko. Fifth Working Conference on Verified Software: Theories, Tools and Experiments, May 2013, Atherton, United States. Springer, 8164, pp.191-201, 2013. 〈hal-00875395〉
  • Daisuke Ishii, Guillaume Melquiond, Shin Nakajima. Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. Einar Broch Johnsen and Luigia Petre. iFM - 10th International Conference on Integrated Formal Methods - 2013, Jun 2013, Turku, Finland. Springer, 7940, pp.139-153, 2013, 〈10.1007/978-3-642-38613-8_10〉. 〈hal-00806701〉
  • Guillaume Melquiond. Automations for verifying floating-point algorithms. 5th Coq Workshop, Jul 2013, Rennes, France. 〈hal-01110666〉
  • 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. Bernhard Gramlich and Dale Miller and Uli Sattler. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.67-81, 2012, 〈10.1007/978-3-642-31365-3_8〉. 〈hal-00687640v2〉
  • Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives. Chris Hawblitzel and Dale Miller. CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. Springer, 7679, pp.289-304, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35308-6_22〉. 〈hal-00712938v2〉
  • Sylvie Boldo, Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. Valérie Berthé and Christiane Frougny and Natacha Portier and Marie-Françoise Roy and Anne Siegel. École des Jeunes Chercheurs en Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30, 2012. 〈hal-00755333〉
  • 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. 2012. 〈hal-00642206v2〉
  • Sylvie Boldo, Guillaume Melquiond. Flocq: A Unified Library for Proving Floating-point Algorithms in Coq. Elisardo Antelo and David Hough and Paolo Ienne. 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. Matt Kaufmann and Lawrence C. Paulson. ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. Springer, 6172, pp.147-162, 2010, Lecture Notes in Computer Science. 〈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. 5625, pp.59-74, 2009, 〈10.1007/978-3-642-02614-0_10〉. 〈inria-00432726〉
  • Guillaume Melquiond. Proving bounds on real-valued functions with computations. Alessandro Armando, Peter Baumgartner, Gilles Dowek. International Joint Conference on Automated Reasoning, IJCAR 2008, Aug 2008, Sydney, Australia. Springer-Verlag, 5195, pp.2--17, 2008, Lecture Notes in Artificial Intelligence. 〈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. 2005. 〈inria-00344518〉
  • 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. IEEE, pp.188-195, 2005, 〈10.1109/ARITH.2005.25〉. 〈hal-00164621〉
  • Sylvie Boldo, Guillaume Melquiond. When double rounding is odd. 17th IMACS World Congress, Jul 2005, Paris, France. pp.11, 2004. 〈inria-00070603v2〉
  • Marc Daumas, Guillaume Melquiond. Generating formally certified bounds on values and round-off errors. Real Numbers and Computers, 2004, Dagstuhl, Germany. pp.55-70, 2004. 〈inria-00070739〉
  • Hervé Brönnimann, Guillaume Melquiond, Sylvain Pion. The Boost Interval Arithmetic Library. Real Numbers and Computers, 2003, Lyon, France. pp.65-80, 2003. 〈inria-00348711〉

Ouvrage (y compris édition critique et traduction)2 documents

  • 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〉

Autre publication1 document

  • François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. The Why3 platform 0.81. Tutorial and Reference Manual. 2013. 〈hal-00822856〉

Pré-publication, Document de travail1 document

  • Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. 2017. 〈hal-01630143〉

Rapport4 documents

  • Guillaume Melquiond, Sylvain Pion. Directed Rounding Arithmetic Operations in C++. [Research Report] RR-6757, INRIA. 2008, pp.11. 〈inria-00345094〉
  • 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〉
  • 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〉
  • Florent De Dinechin, Christoph Lauter, Guillaume Melquiond. Assisted verification of elementary functions. RR-5683, INRIA. 2005, pp.17. 〈inria-00070330〉

Thèse1 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〉