Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Publications : Guillaume Melquiond

Back
melquiond
[23] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives. In Proceedings of the The Second International Conference on Certified Programs and Proofs, Kyoto, Japan, December 2012. [ bib | full paper on HAL ]
[22] 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. https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf. [ bib ]
[21] François Bobot, Sylvain Conchon, Evelyne 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 ]
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.

[20] 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. https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf. [ bib ]
[19] 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 paper on HAL ]
[18] 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, 2012. [ bib | full paper on HAL ]
[17] Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, 216:14-23, 2012. [ bib | DOI ]
[16] 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, 2012. Accepted for publication. http://hal.inria.fr/hal-00649240/en/. [ bib | full paper on HAL ]
[15] 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, Manchester, UK, 2012. http://smt2012.loria.fr/. [ bib ]
[14] 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. http://hal.inria.fr/hal-00649240/en/. [ bib | full paper on HAL | .pdf ]
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
[13] 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.lri.fr/. [ bib ]
[12] 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 paper on HAL ]
[11] 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 | .pdf ]
[10] Érik Martin-Dorel, Guillaume Melquiond, and Jean-Michel Muller. Some issues related to double roundings. Technical report, INRIA, 2011. [ bib | full paper on HAL ]
[9] 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 Matt Kaufmann and Lawrence C. Paulson, editors, Proceedings of the first Interactive Theorem Proving Conference, volume 6172 of LNCS, pages 147-162, Edinburgh, Scotland, July 2010. Springer. (merge of TPHOLs and ACL2). [ bib | full paper on HAL ]
[8] 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 ]
[7] Marc Daumas and Guillaume Melquiond. Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software, 37(1), 2010. [ bib | DOI | full paper on HAL ]
[6] 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 ]
[5] 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 | full paper on HAL | PDF ]
[4] 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 ]
[3] Guillaume Melquiond and Sylvain Pion. Directed rounding arithmetic operations. Technical Report 2899, ISO C++ Standardization Committee, 2009. [ bib ]
[2] 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 | full paper on HAL | PDF ]
[1] 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 ]

Back
This page was generated by bibtex2html.