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 uptodate informations about our team.
Publications : Guillaume Melquiond
Back[23]  Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving Real Analysis in Coq: a UserFriendly 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, JeanChristophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.73. LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.73 edition, July 2012. https://gforge.inria.fr/docman/view.php/2990/8052/manual0.73.pdf. [ bib ] 
[21] 
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala,
Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond.
A Simplexbased extension of FourierMotzkin 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 6781, Manchester, UK, June 2012. Springer.
[ bib 
DOI ]
This paper describes a novel decision procedure for quantifierfree linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g. OmegaTest) or by branching/cutting methods (branchandbound, branchandcut, 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 AltErgo theorem prover. Experimental results are promising and show that our approach is competitive with stateoftheart SMT solvers.

[20]  François Bobot, JeanChristophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.72. LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.72 edition, May 2012. https://gforge.inria.fr/docman/view.php/2990/7919/manual0.72.pdf. [ bib ] 
[19]  Catherine Lelay and Guillaume Melquiond. Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert. In Vingttroisiè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 MasserGramain constant to four decimal digits: delta=1.819.... Mathematics of Computation, 2012. [ bib  full paper on HAL ] 
[17]  Guillaume Melquiond. Floatingpoint arithmetic in the Coq system. Information and Computation, 216:1423, 2012. [ bib  DOI ] 
[16]  Sylvie Boldo, François Clément, JeanChristophe 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/hal00649240/en/. [ bib  full paper on HAL ] 
[15]  Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. Builtin treatment of an axiomatic floatingpoint 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, JeanChristophe 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/hal00649240/en/.
[ bib 
full paper on HAL 
.pdf ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the onedimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floatingpoint computation leads to roundoff errors. We formally specify in Coq the numerical scheme, prove both the method error and the roundoff 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 machinechecked. 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, JeanChristophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform. LRI, CNRS & Univ. ParisSud & INRIA Saclay, version 0.64 edition, February 2011. http://why3.lri.fr/. [ bib ] 
[12]  Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Certifying the floatingpoint implementation of an elementary function using Gappa. IEEE Transactions on Computers, 60(2):242253, 2011. [ bib  DOI  full paper on HAL ] 
[11]  Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floatingpoint algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243252, Tübingen, Germany, 2011. [ bib  .pdf ] 
[10]  Érik MartinDorel, Guillaume Melquiond, and JeanMichel Muller. Some issues related to double roundings. Technical report, INRIA, 2011. [ bib  full paper on HAL ] 
[9]  Sylvie Boldo, François Clément, JeanChristophe 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 147162, Edinburgh, Scotland, July 2010. Springer. (merge of TPHOLs and ACL2). [ bib  full paper on HAL ] 
[8]  JeanMichel Muller, Nicolas Brisebarre, Florent de Dinechin, ClaudePierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres. Handbook of FloatingPoint 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, JeanChristophe Filliâtre, and Guillaume Melquiond. Combining Coq and Gappa for Certifying FloatingPoint Programs. In 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, volume 5625 of Lecture Notes in Artificial Intelligence, pages 5974, 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):419431, 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 231234, 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 CorrectlyRounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Transactions on Computers, 57(4):462471, 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 IMACSGAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Duisburg,Germany, sep 2006. [ bib  http ] 
Back
This page was generated by bibtex2html.