Wiki Agenda Contact Version française

Publications : Guillaume Melquiond

Back
[74] Guillaume Melquiond and Raphaël Rieu-Helft. WhyMP, a formally verified arbitrary-precision integer library. Journal of Symbolic Computation, 115:74--95, 2023. [ bib | DOI | full text on HAL ]
[73] Paul Geneau de Lamarlière, Guillaume Melquiond, and Florian Faissole. Slimmer formal proofs for mathematical libraries. In Int. Conf. on Computer Arithmetic, 2023. [ bib | full text on HAL ]
[72] Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, and Jean-Michel Muller. Floating-point arithmetic. Acta Numerica, 32:203--290, 2023. [ bib | DOI | full text on HAL ]
[71] Érik Martin-Dorel, Guillaume Melquiond, and Pierre Roux. Enabling floating-point arithmetic in the Coq proof assistant. Journal of Automated Reasoning, 67(33), 2023. [ bib | DOI | full text on HAL ]
[70] Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A strong call-by-need calculus. Logical Methods in Computer Science, 19(1), 2023. [ bib | DOI | full text on HAL ]
[69] Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A strong call-by-need calculus. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, volume 195, pages 9:1--9:22, 2021. [ bib | DOI | full text on HAL ]
[68] Sylvie Boldo and Guillaume Melquiond. Some formal tools for computer arithmetic: Flocq and Gappa. In Mioara Joldes and Fabrizio Lamberti, editors, 28th IEEE International Symposium on Computer Arithmetic, 2021. [ bib | full text on HAL ]
[67] Guillaume Melquiond. Plotting in a formally verified way. In 6th Workshop on Formal Integrated Development Environment, volume 338, pages 39--45, 2021. [ bib | DOI | full text on HAL ]
[66] Guillaume Melquiond and Raphaël Rieu-Helft. WhyMP, a formally verified arbitrary-precision integer library. In 45th International Symposium on Symbolic and Algebraic Computation (ISSAC), pages 352--359, 2020. [ bib | DOI | full text on HAL ]
Keywords: Integer arithmetic ; Deductive program verification ; Mathematical library
[65] Guillaume Melquiond and Raphaël Rieu-Helft. Formal verification of a state-of-the-art integer square root. In Symposium on Computer Arithmetic, pages 183--186, Kyoto, Japan, June 2019. [ bib | full text on HAL ]
[64] Guillaume Melquiond. Formal Verification for Numerical Computations, and the Other Way Around. Habilitation à diriger des recherches, Université Paris Sud, April 2019. [ bib | full text on HAL ]
[63] Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally verified approximations of definite integrals. Journal of Automated Reasoning, 62(2):281--300, February 2019. [ bib | DOI | full text on HAL ]
[62] Guillaume Melquiond. Computer arithmetic and formal proofs. In Nicolas Magaud and Zaynah Dargaye, editors, Trentièmes Journées Francophones des Langages Applicatifs, Les Rousses, France, January 2019. [ bib | full text on HAL ]
[61] Guillaume Melquiond and Raphaël Rieu-Helft. A Why3 framework for reflection proofs and its application to GMP's algorithms. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, 9th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science, Oxford, United Kingdom, July 2018. [ bib | full text on HAL ]
[60] Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, and Serge Torres. Handbook of Floating-point Arithmetic (2nd edition). Birkhäuser Basel, July 2018. [ bib | DOI | full text on HAL ]
Keywords: arithmetic operators ; arithmetic algorithms ; numerical computing ; floating-point arithmetic ; computer arithmetic
[59] Sylvie Boldo and Guillaume Melquiond. Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. ISTE Press - Elsevier, December 2017. [ bib | full text on HAL ]
[58] Raphaël Rieu-Helft, Claude Marché, and Guillaume Melquiond. How to get an efficient yet verified arbitrary-precision integer library. In 9th Working Conference on Verified Software: Theories, Tools, and Experiments, volume 10712 of Lecture Notes in Computer Science, pages 84--101, Heidelberg, Germany, July 2017. [ bib | DOI | full text on HAL | .pdf ]
Keywords: arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier
[57] Sylvain Conchon, Mohamed Iguernlala, Kailiang Ji, Guillaume Melquiond, and Clément Fumex. A three-tier strategy for reasoning about floating-point numbers in SMT. In Computer Aided Verification, volume 10427 of Lecture Notes in Computer Science, pages 419--435, 2017. [ bib | DOI | full text on HAL ]
[56] Assia Mahboubi, Guillaume Melquiond, and Thomas Sibut-Pinote. Formally verified approximations of definite integrals. In Jasmin Christian Blanchette and Stephan Merz, editors, Proceedings of the 7th International Conference on Interactive Theorem Proving, volume 9807 of Lecture Notes in Computer Science, Nancy, France, August 2016. [ bib | DOI | full text on HAL | .pdf ]
[55] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science, 2016. [ bib | full text on HAL ]
[54] Érik Martin-Dorel and Guillaume Melquiond. Proving tight bounds on univariate expressions with elementary functions in Coq. Journal of Automated Reasoning, 2016. [ bib | DOI | full text on HAL ]
Keywords: Coq proof assistant ; formal proof ; decision procedure ; interval arithmetic ; floating-point arithmetic ; nonlinear arithmetic
[53] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 9(1):41--62, June 2015. [ bib | DOI | full text on HAL ]
[52] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.86.1. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.86.1 edition, May 2015. http://why3.org/download/manual-0.86.1.pdf. [ bib | .pdf ]
[51] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, 54(2):135--163, February 2015. [ bib | full text on HAL ]
[50] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. Computers and Mathematics with Applications, 68(3):325--352, 2014. [ bib | DOI | full text on HAL | http ]
[49] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.82. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.82 edition, December 2013. http://why3.org/download/manual-0.82.pdf. [ bib | .pdf ]
[48] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. Preserving user proofs across specification changes. In Ernie Cohen and Andrey Rybalchenko, editors, Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE), volume 8164 of Lecture Notes in Computer Science, pages 191--201, Atherton, USA, May 2013. Springer. [ bib | full text on HAL ]
Keywords: Why3
[47] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, 50(4):423--456, April 2013. [ bib | DOI | full text on HAL ]
[46] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.81. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.81 edition, March 2013. http://why3.org/download/manual-0.81.pdf. [ bib | full text on HAL | .pdf ]
Keywords: Why3
[45] Guillaume Melquiond, Werner Georg Nowak, and Paul Zimmermann. Numerical approximation of the Masser-Gramain constant to four decimal digits: delta=1.819.... Mathematics of Computation, 82:1235--1246, 2013. [ bib | DOI | full text on HAL ]
[44] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013. [ bib | full text on HAL ]
[43] Sylvie Boldo and Guillaume Melquiond. Informatique Mathématique, une photographie en 2013, chapter Arithmétique des ordinateurs et preuves formelles, pages 189--220. Presses Universitaires de Perpignan, Perpignan, France, 2013. [ bib | full text on HAL ]
[42] Daisuke Ishii, Guillaume Melquiond, and Shin Nakajima. Inductive verification of hybrid automata with strongest postcondition calculus. In Einar Broch Johnsen and Luigia Petre, editors, Proceedings of the 10th Conference on Integrated Formal Methods, volume 7940 of Lecture Notes in Computer Science, pages 139--153, Turku, Finland, 2013. [ bib | DOI | full text on HAL ]
[41] Érik Martin-Dorel, Guillaume Melquiond, and Jean-Michel Muller. Some issues related to double roundings. BIT Numerical Mathematics, 53(4):897--924, 2013. [ bib | DOI | full text on HAL ]
[40] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving real analysis in Coq: a user-friendly approach to integrals and derivatives. In Chris Hawblitzel and Dale Miller, editors, Proceedings of the Second International Conference on Certified Programs and Proofs, volume 7679 of Lecture Notes in Computer Science, pages 289--304, Kyoto, Japan, December 2012. [ bib | DOI | full text on HAL ]
[39] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.80. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.80 edition, October 2012. https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf. [ bib | .pdf ]
Keywords: Why3
[38] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.73. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.73 edition, July 2012. [ bib | .pdf ]
Keywords: Why3
[37] François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond. A Simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors, IJCAR 2012: Proceedings of the 6th International Joint Conference on Automated Reasoning, volume 7364 of Lecture Notes in Computer Science, pages 67--81, Manchester, UK, June 2012. Springer. [ bib | DOI | full text on HAL ]
This paper describes a novel decision procedure for quantifier-free linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g. Omega-Test) or by branching/cutting methods (branch-and-bound, branch-and-cut, Gomory cuts). Our approach tries to bridge the gap between the two techniques: it interleaves an exhaustive search for a model with bounds inference. These bounds are computed provided an oracle capable of finding constant positive linear combinations of affine forms. We also show how to design an efficient oracle based on the Simplex procedure. Our algorithm is proved sound, complete, and terminating and is implemented in the Alt-Ergo theorem prover. Experimental results are promising and show that our approach is competitive with state-of-the-art SMT solvers.

[36] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.72. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.72 edition, May 2012. [ bib | .pdf ]
Keywords: Why3
[35] Sylvie Boldo and Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. In Valérie Berthé, Christiane Frougny, Natacha Portier, Marie-Françoise Roy, and Anne Siegel, editors, École des Jeunes Chercheurs en Informatique Mathématique, pages 1--30. Rennes, France, March 2012. [ bib | full text on HAL ]
[34] Catherine Lelay and Guillaume Melquiond. Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert. In Vingt-troisièmes Journées Francophones des Langages Applicatifs, Carnac, France, February 2012. [ bib | full text on HAL ]
[33] Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 216:14--23, 2012. [ bib | DOI | full text on HAL ]
[32] Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. Built-in treatment of an axiomatic floating-point theory for SMT solvers. In Pascal Fontaine and Amit Goel, editors, SMT workshop, pages 12--21, Manchester, UK, 2012. LORIA. [ bib ]
[31] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: Mathematics and program. Research Report 7826, INRIA, December 2011. [ bib | full text on HAL ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machine-checked.

Keywords: Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis
[30] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edition, February 2011. http://why3.org/. [ bib ]
Keywords: Why3
[29] Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Transactions on Computers, 60(2):242--253, 2011. [ bib | DOI | full text on HAL ]
[28] Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243--252, Tübingen, Germany, 2011. [ bib | DOI | full text on HAL ]
[27] Marc Daumas and Guillaume Melquiond. Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software, 37(1):1--20, 2010. [ bib | DOI | .pdf ]
Keywords: Gappa
[26] Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres. Handbook of Floating-Point Arithmetic. Birkhäuser, 2010. [ bib ]
[25] Marc Daumas and Guillaume Melquiond. Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software, 37(1):1--20, 2010. [ bib | DOI | full text on HAL ]
[24] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal proof of a wave equation resolution scheme: the method error. In Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 147--162. Springer, 2010. [ bib | DOI | full text on HAL ]
[23] Sylvie Boldo, Jean-Christophe Filliâtre, and Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. In 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, volume 5625 of Lecture Notes in Artificial Intelligence, pages 59--74, Grand Bend, Canada, July 2009. Springer. [ bib | DOI ]
[22] Siegfried M. Rump, Paul Zimmermann, Sylvie Boldo, and Guillaume Melquiond. Computing predecessor and successor in rounding to nearest. BIT, 49(2):419--431, June 2009. [ bib | DOI | full text on HAL ]
[21] William Edmonson and Guillaume Melquiond. IEEE interval standard working group - P1788: current status. In Javier D. Bruguera, Marius Cornea, Debjit DasSarma, and John Harrison, editors, Proceedings of the 19th IEEE Symposium on Computer Arithmetic, pages 231--234, Portland, OR, USA, 2009. [ bib | DOI ]
[20] Guillaume Melquiond and Sylvain Pion. Directed rounding arithmetic operations. Technical Report 2899, ISO C++ Standardization Committee, 2009. [ bib ]
[19] Guillaume Melquiond. Floating-point arithmetic in the Coq system. In Proceedings of the 8th Conference on Real Numbers and Computers, pages 93--102, Santiago de Compostela, Spain, 2008. [ bib | PDF ]
[18] Guillaume Melquiond. Proving bounds on real-valued functions with computations. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Proceedings of the 4th International Joint Conference on Automated Reasoning, volume 5195 of Lecture Notes in Artificial Intelligence, pages 2--17, Sydney, Australia, 2008. [ bib | PDF ]
[17] Sylvie Boldo and Guillaume Melquiond. Emulation of FMA and Correctly-Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Transactions on Computers, 57(4):462--471, 2008. [ bib | DOI | full text on HAL ]
[16] Guillaume Melquiond and Sylvain Pion. Formally certified floating-point filters for homogeneous geometric predicates. Theoretical Informatics and Applications, 41(1):57--70, 2007. [ bib ]
[15] Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Assisted verification of elementary functions using Gappa. In Proceedings of the 2006 ACM Symposium on Applied Computing, pages 1318--1322, Dijon, France, 2006. [ bib | .pdf ]
[14] Hervé Brönnimann, Guillaume Melquiond, and Sylvain Pion. The design of the Boost interval arithmetic library. Theoretical Computer Science, 351:111--118, 2006. [ bib ]
[13] Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Assisted verification of elementary functions using Gappa. In Proceedings of the 2006 ACM Symposium on Applied Computing, pages 1318--1322, Dijon, France, 2006. [ bib | PDF ]
[12] Hervé Brönnimann, Guillaume Melquiond, and Sylvain Pion. Bool_set: multi-valued logic. Technical Report 2136, ISO C++ Standardization Committee, 2006. [ bib ]
[11] Hervé Brönnimann, Guillaume Melquiond, and Sylvain Pion. A proposal to add interval arithmetic to the C++ standard library. Technical Report 2137, ISO C++ Standardization Committee, 2006. [ bib ]
[10] Hervé Brönnimann, Guillaume Melquiond, and Sylvain Pion. Proposing interval arithmetic for the c++ standard. In Proceedings of the 12th GAMM - IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Duisburg, Germany, 2006. [ bib ]
[9] Guillaume Melquiond. De l'arithmétique d'intervalles à la certification de programmes. PhD thesis, École Normale Supérieure de Lyon, Lyon, France, 2006. [ bib ]
[8] Sylvie Boldo, Marc Daumas, William Kahan, and Guillaume Melquiond. Proof and certification for an accurate discriminant. In 12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Duisburg,Germany, sep 2006. [ bib | http ]
[7] Marc Daumas, Guillaume Melquiond, and César Muñoz. Guaranteed proofs using interval arithmetic. In Paolo Montuschi and Eric Schwarz, editors, 17th IEEE Symposium on Computer Arithmetic, pages 188--195, Cape Cod, MA, USA, 2005. [ bib | .pdf ]
[6] Marc Daumas, Guillaume Melquiond, and César Muñoz. Guaranteed proofs using interval arithmetic. In Paolo Montuschi and Eric Schwarz, editors, Proceedings of the 17th IEEE Symposium on Computer Arithmetic, pages 188--195, Cape Cod, Massachusetts, USA, 2005. [ bib ]
[5] Sylvie Boldo and Guillaume Melquiond. When double rounding is odd. In Proceedings of the 17th IMACS World Congress on Computational and Applied Mathematics, Paris, France, 2005. [ bib | .ps ]
[4] Guillaume Melquiond and Sylvain Pion. Formal certification of arithmetic filters for geometric predicates. In Proceedings of the 17th IMACS World Congress on Computational and Applied Mathematics, Paris, France, 2005. [ bib ]
[3] Marc Daumas and Guillaume Melquiond. Generating formally certified bounds on values and round-off errors. In Vasco Brattka, Christiane Frougny, and Norbert Müller, editors, Proceedings of the 6th Conference on Real Numbers and Computers, pages 55--70, Schloß Dagstuhl, Germany, 2004. [ bib ]
[2] Hervé Brönnimann, Guillaume Melquiond, and Sylvain Pion. The Boost interval arithmetic library. In Proceedings of the 5th Conference on Real Numbers and Computers, pages 65--80, Lyon, France, 2003. [ bib ]
[1] François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform. http://why3.org/. [ bib ]
Keywords: Why3
Back
This page was generated by bibtex2html.