Mots-clés

Nombre de documents

41

Guillaume Melquiond's Publications


Brought to you by HAL.


Article dans une revue15 documents

  • 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>
  • É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, 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, 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, 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>
  • 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>
  • 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. 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ès19 documents

  • 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>
  • Guillaume Melquiond. Automations for verifying floating-point algorithms. 5th Coq Workshop, Jul 2013, Rennes, France. <hal-01110666>
  • 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>
  • 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>
  • 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>
  • 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>
  • 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; Certified Programs and Proofs. <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. 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; Interactive Theorem Proving. <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>
  • 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>
  • 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. 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)1 document

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

Rapport4 documents

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

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>