melquiond.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc melquiond.cite -ob melquiond.bib -c 'author : "melquiond"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@article{DauMel09,
author = {Marc Daumas and Guillaume Melquiond},
title = {Certification of bounds on expressions involving rounded operators},
journal = {Transactions on Mathematical Software},
publisher = {ACM},
year = {2010},
volume = {37},
number = {1},
pages = {1--20},
doi = {10.1145/1644001.1644003},
url = {http://www.lri.fr/~melquion/doc/09-toms.pdf},
keywords = {Gappa}
}
@inproceedings{DauMelMun05,
author = {Marc Daumas and Guillaume Melquiond and C\'esar Mu{\~n}oz},
title = {Guaranteed proofs using interval arithmetic},
booktitle = {17th IEEE Symposium on Computer Arithmetic},
editor = {Paolo Montuschi and Eric Schwarz},
pages = {188--195},
address = {Cape Cod, MA, USA},
year = {2005},
url = {http://www.lri.fr/~melquion/doc/05-arith17-article.pdf}
}
@inproceedings{DinLauMel06,
author = {Florent de Dinechin and Christoph Lauter and Guillaume Melquiond},
title = {Assisted verification of elementary functions using {G}appa},
booktitle = {Proceedings of the 2006 ACM Symposium on Applied Computing},
pages = {1318--1322},
address = {Dijon, France},
year = {2006},
url = {http://www.lri.fr/~melquion/doc/06-mcms-article.pdf}
}
@inproceedings{bronnimann03rnc,
author = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
title = {The {B}oost interval arithmetic library},
booktitle = {Proceedings of the 5th Conference on Real Numbers and Computers},
pages = {65--80},
address = {Lyon, France},
year = {2003},
x-type = {article},
x-support = {actes},
x-cle-support = {RNC}
}
@inproceedings{daumas04rnc,
author = {Marc Daumas and Guillaume Melquiond},
title = {Generating formally certified bounds on values and round-off errors},
booktitle = {Proceedings of the 6th Conference on Real Numbers and Computers},
editor = {Vasco Brattka and Christiane Frougny and Norbert M{\"u}ller},
pages = {55--70},
address = {Schlo{\ss} Dagstuhl, Germany},
year = {2004},
x-type = {article},
x-support = {actes},
x-cle-support = {RNC}
}
@inproceedings{daumas05arith,
author = {Marc Daumas and Guillaume Melquiond and C{\'e}sar Mu{\~n}oz},
title = {Guaranteed proofs using interval arithmetic},
booktitle = {Proceedings of the 17th IEEE Symposium on Computer Arithmetic},
editor = {Paolo Montuschi and Eric Schwarz},
pages = {188--195},
address = {Cape Cod, Massachusetts, USA},
year = {2005},
x-type = {article},
x-support = {actes},
x-cle-support = {ARITH}
}
@inproceedings{boldo05imacs,
author = {Sylvie Boldo and Guillaume Melquiond},
title = {When double rounding is odd},
booktitle = {Proceedings of the 17th IMACS World Congress on Computational and Applied Mathematics},
address = {Paris, France},
year = {2005},
url = {http://www.lri.fr/~sboldo/files/imacs05.ps},
x-type = {article},
x-support = {actes}
}
@inproceedings{melquiond05imacs,
author = {Guillaume Melquiond and Sylvain Pion},
title = {Formal certification of arithmetic filters for geometric predicates},
booktitle = {Proceedings of the 17th IMACS World Congress on Computational and Applied Mathematics},
address = {Paris, France},
x-type = {article},
x-support = {actes},
year = {2005}
}
@article{bronnimann06tcs,
author = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
title = {The design of the {B}oost interval arithmetic library},
journal = {Theoretical Computer Science},
editor = {Marc Daumas and Nathalie Revol},
pages = {111--118},
volume = {351},
year = {2006},
x-type = {article},
x-support = {revue},
x-cle-support = {TCS}
}
@inproceedings{dedinechin06sac,
author = {Florent de Dinechin and Christoph Lauter and Guillaume Melquiond},
title = {Assisted verification of elementary functions using {G}appa},
booktitle = {Proceedings of the 2006 ACM Symposium on Applied Computing},
pages = {1318--1322},
address = {Dijon, France},
year = {2006},
x-type = {article},
x-support = {actes},
x-cle-support = {SAC},
x-pdf = {http://www.lri.fr/~melquion/doc/06-mcms-article.pdf}
}
@techreport{bronnimann06rr1,
author = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
title = {Bool\_set: multi-valued logic},
institution = {ISO C++ Standardization Committee},
number = {2136},
year = {2006},
x-type = {article},
x-support = {rapport}
}
@techreport{bronnimann06rr2,
author = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
title = {A Proposal to add Interval Arithmetic to the {C}++ Standard Library},
institution = {ISO C++ Standardization Committee},
number = {2137},
year = {2006},
x-type = {article},
x-support = {rapport}
}
@inproceedings{bronnimann06scan,
author = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
title = {Proposing Interval Arithmetic for the C++ Standard},
booktitle = {Proceedings of the 12th GAMM - IMACS International Symposium on
Scientific Computing, Computer Arithmetic and Validated Numerics},
address = {Duisburg, Germany},
year = {2006},
x-type = {article},
x-support = {actes},
x-cle-support = {SCAN}
}
@phdthesis{melquiond06phd,
author = {Guillaume Melquiond},
title = {De l'arithm{\'e}tique d'intervalles {\`a} la certification de programmes},
school = {{\'E}cole {N}ormale {S}up{\'e}rieure de {L}yon},
address = {Lyon, France},
year = {2006},
x-type = {these},
x-support = {rapport}
}
@article{melquiond07tia,
author = {Guillaume Melquiond and Sylvain Pion},
title = {Formally certified floating-point filters for homogeneous geometric predicates},
journal = {Theoretical Informatics and Applications},
editor = {Vasco Brattka and Christiane Frougny and Norbert Mueller},
year = {2007},
volume = {41},
number = {1},
pages = {57--70},
x-type = {article},
x-support = {revue}
}
@inproceedings{melquiond08rnc,
author = {Guillaume Melquiond},
title = {Floating-point arithmetic in the {C}oq system},
booktitle = {Proceedings of the 8th Conference on Real Numbers and Computers},
address = {Santiago de Compostela, Spain},
year = {2008},
pages = {93--102},
x-type = {article},
x-support = {actes},
x-cle-support = {RNC},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-pdf = {http://www.lri.fr/~melquion/doc/08-rnc8-article.pdf}
}
@inproceedings{melquiond08ijcar,
author = {Guillaume Melquiond},
title = {Proving bounds on real-valued functions with computations},
booktitle = {Proceedings of the 4th International Joint Conference on Automated Reasoning},
editor = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
address = {Sydney, Australia},
year = {2008},
volume = {5195},
pages = {2--17},
series = {Lecture Notes in Artificial Intelligence},
x-type = {article},
x-support = {actes},
x-cle-support = {IJCAR},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-pdf = {http://www.lri.fr/~melquion/doc/08-ijcar-article.pdf}
}
@article{boldo14jar,
author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
title = {{Verified Compilation of Floating-Point Computations}},
journal = {Journal of Automated Reasoning},
volume = {54},
number = {2},
pages = {135-163},
year = {2015},
month = feb,
publisher = {{Springer Verlag (Germany)}},
hal = {https://hal.inria.fr/hal-00862689},
topics = {team,lri},
type_publi = {irevcomlec}
}
@article{boldo14camwa,
title = {{Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program}},
author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Filli{\^a}tre, Jean-Christophe and Mayero, Micaela and Melquiond, Guillaume and Weis, Pierre},
year = {2014},
volume = {68},
number = {3},
pages = {325--352},
journal = {Computers and Mathematics with Applications},
hal = {http://hal.inria.fr/hal-00769201},
url = {http://www.sciencedirect.com/science/article/pii/S0898122114002636},
doi = {10.1016/j.camwa.2014.06.004},
topics = {team,lri},
type_publi = {irevcomlec}
}
@article{BLM14mcs,
author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
title = {Coquelicot: A User-Friendly Library of Real Analysis for {C}oq},
hal = {http://hal.inria.fr/hal-00860648},
journal = {Mathematics in Computer Science},
topics = {team},
issn = {1661-8270},
doi = {10.1007/s11786-014-0181-1},
month = jun,
year = {2015},
volume = {9},
number = {1},
publisher = {Springer Basel},
pages = {41-62}
}
@article{BLM14mscs,
author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
title = {Formalization of Real Analysis: A Survey of Proof Assistants and Libraries},
year = {2016},
hal = {http://hal.inria.fr/hal-00806920},
journal = {Mathematical Structures in Computer Science},
topics = {team}
}
@article{bol08tc1,
author = {Sylvie Boldo and Guillaume Melquiond},
title = {Emulation of {FMA} and {C}orrectly-{R}ounded {S}ums: {P}roved {A}lgorithms {U}sing {R}ounding to {O}dd},
journal = {IEEE Transactions on Computers},
year = {2008},
volume = {57},
number = {4},
pages = {462--471},
topics = {team,lri},
type_digiteo = {revue_cl},
type_publi = {irevcomlec},
hal = {http://hal.inria.fr/inria-00080427/},
doi = {10.1109/TC.2007.70819},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {ITComputers},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@inproceedings{boldo06scan,
author = {Sylvie Boldo and Marc Daumas and William Kahan and
Guillaume Melquiond},
title = {Proof and certification for an accurate discriminant},
booktitle = {12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics},
year = {2006},
address = {Duisburg,Germany},
topics = {team},
type_publi = {colloque},
url = {http://scan2006.uni-due.de/show_abstracts.php?title=+Proof+and+certification+for+an+accurate+discriminant},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes_aux},
x-cle-support = {SCAN},
month = {sep}
}
@article{bolmel09bit,
author = {Siegfried M. Rump and Paul Zimmermann and Sylvie Boldo and Guillaume Melquiond},
title = {Computing predecessor and successor in rounding to nearest},
journal = {BIT},
year = {2009},
volume = {49},
number = {2},
month = jun,
pages = {419--431},
doi = {10.1007/s10543-009-0218-z},
hal = {http://hal.inria.fr/inria-00337537/},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {revue},
x-pays = {DE},
x-international-audience = {yes},
x-editorial-board = {yes}
}
@inproceedings{boldo09calculemus,
author = {Sylvie Boldo and Jean-Christophe Filli\^atre and Guillaume Melquiond},
title = {Combining {C}oq and {G}appa for {C}ertifying {F}loating-{P}oint
{P}rograms },
booktitle = {16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning},
pages = {59--74},
year = {2009},
month = jul,
volume = {5625},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
address = {Grand Bend, Canada},
doi = {10.1007/978-3-642-02614-0_10},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-support = {actes},
topics = {team}
}
@book{muller09book,
author = {Jean-Michel Muller and Nicolas Brisebarre and Florent de Dinechin and Claude-Pierre Jeannerod and Vincent Lef{\`e}vre and Guillaume Melquiond and Nathalie Revol and Damien Stehl{\'e} and Serge Torres},
title = {Handbook of Floating-Point Arithmetic},
publisher = {Birkh{\"a}user},
year = {2010},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-support = {livre},
x-type = {livre},
type_publi = {ouvrage}
}
@article{daumas09toms,
author = {Marc Daumas and Guillaume Melquiond},
title = {Certification of bounds on expressions involving rounded operators},
journal = {Transactions on Mathematical Software},
publisher = {ACM Press},
year = {2010},
volume = {37},
number = {1},
topics = {team},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {TOMS},
x-international-audience = {yes},
x-editorial-board = {yes},
type_publi = {irevcomlec},
pages = {1--20},
doi = {10.1145/1644001.1644003},
hal = {hal-00127769}
}
@inproceedings{edmonson09arith,
author = {William Edmonson and Guillaume Melquiond},
title = {{IEEE} interval standard working group - {P1788}: current status},
booktitle = {Proceedings of the 19th IEEE Symposium on Computer Arithmetic},
editor = {Javier D. Bruguera and Marius Cornea and Debjit DasSarma and John Harrison},
address = {Portland, OR, USA},
year = {2009},
pages = {231--234},
doi = {10.1109/ARITH.2009.36},
topics = {team},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-pays = {US},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
type_publi = {icolcomlec}
}
@inproceedings{boldo10-itp,
author = {Sylvie Boldo and Fran\c{c}ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
title = {Formal Proof of a Wave Equation Resolution Scheme: the Method Error},
booktitle = {Interactive Theorem Proving},
year = 2010,
series = {Lecture Notes in Computer Science},
x-address = {Edinburgh, Scotland},
x-month = jul,
publisher = {Springer},
x-editor = {Matt Kaufmann and Lawrence C. Paulson},
volume = 6172,
pages = {147--162},
hal = {http://hal.inria.fr/inria-00450789/en},
doi = {10.1007/978-3-642-14052-5_12/},
x-equipes = {demons PROVAL ext},
x-support = {actes},
x-cle-support = {ITProving},
x-type = {article},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-editorial-board = {yes}
}
@article{dinechin10tc,
hal = {http://hal.inria.fr/inria-00533968/en/},
title = {Certifying the floating-point implementation of an elementary function using {G}appa},
author = {de Dinechin, Florent and Lauter, Christoph and Melquiond, Guillaume},
publisher = {{IEEE} Comp. Soc. Press},
journal = {{IEEE} {T}ransactions on {C}omputers },
pages = {242--253},
volume = {60},
number = {2},
x-equipes = {demons PROVAL ext},
x-international-audience = {yes},
x-editorial-board = {yes},
x-pays = {US},
topics = {team},
doi = {10.1109/TC.2010.128},
year = 2011
}
@techreport{melquiond09cxx,
author = {Guillaume Melquiond and Sylvain Pion},
title = {Directed rounding arithmetic operations},
institution = {ISO C++ Standardization Committee},
number = {2899},
year = {2009},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {rapport},
topics = {team}
}
@manual{bobot11why3,
title = {The Why3 platform},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.64},
month = feb,
year = 2011,
topics = {team},
keywords = {Why3},
note = {\url{http://why3.org/}}
}
@misc{why3,
title = {The {Why3} platform},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
topics = {team},
keywords = {Why3},
note = {\url{http://why3.org/}}
}
@manual{why3manual072,
title = {The Why3 platform, version 0.72},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.72},
month = may,
year = 2012,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
pdf = {https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf},
rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf}}
}
@manual{why3manual073,
title = {The Why3 platform, version 0.73},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.73},
month = jul,
year = 2012,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
pdf = {https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf},
rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf}}
}
@manual{why3manual080,
title = {The Why3 platform, version 0.80},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.80},
month = oct,
year = 2012,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons PROVAL},
pdf = {https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf},
note = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}},
rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}}
}
@manual{why3manual081,
title = {The Why3 platform, version 0.81},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.81},
month = mar,
year = 2013,
topics = {team},
keywords = {Why3},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons TOCCATA},
pdf = {http://why3.org/download/manual-0.81.pdf},
note = {\url{http://why3.org/download/manual-0.81.pdf}},
hal = {http://hal.inria.fr/hal-00822856/}
}
@manual{why3manual082,
title = {The Why3 platform, version 0.82},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.82},
month = dec,
year = 2013,
topics = {team},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons TOCCATA},
pdf = {http://why3.org/download/manual-0.82.pdf},
note = {\url{http://why3.org/download/manual-0.82.pdf}}
}
@manual{why3manual0861,
title = {The Why3 platform, version 0.86.1},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
edition = {version 0.86.1},
month = may,
year = 2015,
topics = {team},
x-type = {diffusion},
x-support = {manuel},
x-equipes = {demons TOCCATA},
pdf = {http://why3.org/download/manual-0.86.1.pdf},
note = {\url{http://why3.org/download/manual-0.86.1.pdf}}
}
@inproceedings{BolMel11,
author = {Sylvie Boldo and Guillaume Melquiond},
title = {{Flocq}: A Unified Library for Proving Floating-point Algorithms in {Coq}},
booktitle = {Proceedings of the 20th IEEE Symposium on Computer Arithmetic},
editor = {Elisardo Antelo and David Hough and Paolo Ienne},
address = {T{\"u}bingen, Germany},
year = {2011},
pages = {243--252},
doi = {10.1109/ARITH.2011.40},
hal = {http://hal.archives-ouvertes.fr/inria-00534854/},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ARITH},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inproceedings{lelay12jfla,
author = {Catherine Lelay and Guillaume Melquiond},
title = {Diff\'erentiabilit\'e et int\'egrabilit\'e en {C}oq. {A}pplication \`a la formule de d'{A}lembert},
topics = {team, lri},
type_publi = {colcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
crossref = {jfla12},
hal = {http://hal.inria.fr/hal-00642206/fr/}
}
@article{MelNowZim12,
hal = {http://hal.inria.fr/hal-00644166/en/},
title = {Numerical Approximation of the {M}asser-{G}ramain Constant to Four Decimal Digits: delta=1.819\ldots},
author = {Guillaume Melquiond and Werner Georg Nowak and Paul Zimmermann},
publisher = {AMS},
journal = {Mathematics of Computation},
year = {2013},
volume = {82},
pages = {1235--1246},
doi = {10.1090/S0025-5718-2012-02635-4},
topics = {team},
x-type = {article},
x-support = {revue},
x-cle-support = {MoC},
x-international-audience = {yes},
x-editorial-board = {yes},
x-equipes = {demons PROVAL ext},
type_publi = {irevcomlec}
}
@techreport{BCFMMW11rr,
hal_id = {hal-00649240},
hal = {http://hal.inria.fr/hal-00649240/en/},
title = {Wave Equation Numerical Resolution: Mathematics and Program},
author = {Boldo, Sylvie and Cl\'ement, Fran\c{c}ois and Filli{\^a}tre, Jean-Christophe and Mayero, Micaela and Melquiond, Guillaume and Weis, Pierre},
abstract = {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},
language = {Anglais},
affiliation = {PROVAL - INRIA Saclay - Ile de France , Laboratoire de Recherche en Informatique - LRI , ESTIME - INRIA Rocquencourt , Laboratoire d'informatique de Paris-nord - LIPN , ARENAIRE - Inria Grenoble Rh{\^o}ne-Alpes / LIP Laboratoire de l'Informatique du Parall{\'e}lisme},
pages = {30},
type = {Research Report},
institution = {INRIA},
number = 7826,
year = 2011,
month = dec,
topics = {team},
x-equipes = {demons PROVAL ext},
x-support = {rapport}
}
@inproceedings{bobot12ijcar,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and
\'Evelyne Contejean and Mohamed Iguernelala and
Assia Mahboubi and Alain Mebsout and Guillaume Melquiond},
title = {A {Simplex}-Based Extension of {Fourier-Motzkin} for
Solving Linear Integer Arithmetic},
booktitle = {IJCAR 2012: Proceedings of the 6th International Joint
Conference on Automated Reasoning},
year = {2012},
editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
series = {Lecture Notes in Computer Science},
address = {Manchester, UK},
month = jun,
volume = {7364},
pages = {67--81},
hal = {http://hal.inria.fr/hal-00687640},
doi = {10.1007/978-3-642-31365-3_8},
topics = {team},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
x-cle-support = {IJCAR},
type_publi = {icolcomlec},
publisher = {Springer},
abstract = {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.}
}
@article{melquiond12,
author = {Guillaume Melquiond},
title = {Floating-point arithmetic in the {C}oq system},
journal = {Information and Computation},
volume = {216},
pages = {14--23},
year = {2012},
doi = {10.1016/j.ic.2011.09.005},
hal = {http://hal.inria.fr/hal-00797913},
topics = {team},
x-international-audience = {yes},
x-editorial-board = {yes},
x-equipes = {demons PROVAL},
x-support = {revue},
x-cle-support = {JIC},
x-type = {article},
type_publi = {irevcomlec}
}
@article{boldo13jar,
author = {Sylvie Boldo and Fran\c{c}ois Cl\'ement and Jean-Christophe Filli\^atre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
title = {Wave Equation Numerical Resolution:
a Comprehensive Mechanized Proof of a {C} Program},
journal = {Journal of Automated Reasoning},
year = {2013},
volume = {50},
number = {4},
pages = {423--456},
month = apr,
x-international-audience = {yes},
x-editorial-board = {yes},
x-equipes = {demons PROVAL ext},
x-support = {revue},
x-type = {article},
x-cle-support = {JAR},
hal = {http://hal.inria.fr/hal-00649240/en/},
doi = {10.1007/s10817-012-9255-4},
topics = {team}
}
@inproceedings{boldo12cpp,
author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
title = {Improving Real Analysis in {Coq}: a User-Friendly Approach to Integrals and Derivatives},
booktitle = {Proceedings of the Second International Conference on Certified Programs and Proofs},
pages = {289--304},
year = {2012},
editor = {Chris Hawblitzel and Dale Miller},
volume = {7679},
optnumber = {},
series = {Lecture Notes in Computer Science},
address = {Kyoto, Japan},
month = dec,
optorganization = {},
optpublisher = {},
optnote = {},
x-international-audience = {yes},
x-proceedings = {yes},
x-equipes = {demons PROVAL},
x-support = {actes},
x-cle-support = {CPP},
x-type = {article},
hal = {http://hal.inria.fr/hal-00712938},
doi = {10.1007/978-3-642-35308-6_22},
topics = {team}
}
@inproceedings{conchon12smt,
author = {Sylvain Conchon and Guillaume Melquiond and Cody Roux and Mohamed Iguernelala},
title = {Built-in Treatment of an Axiomatic Floating-Point Theory for {SMT} Solvers},
pages = {12--21},
x-equipes = {demons PROVAL},
x-support = {rapport},
x-cle-support = {SMT},
x-type = {article},
crossref = {smt2012},
topics = {team}
}
@incollection{boldo:hal-00755333,
hal = {http://hal.inria.fr/hal-00755333},
title = {Arithm{\'e}tique des ordinateurs et preuves formelles},
author = {Sylvie Boldo and Guillaume Melquiond},
booktitle = {{\'E}cole des Jeunes Chercheurs en Informatique Math{\'e}matique},
pages = {1--30},
address = {Rennes, France},
organization = {GDR Informatique Math{\'e}matique},
editor = {Val{\'e}rie Berth{\'e} and Christiane Frougny and Natacha Portier and Marie-Fran\c{c}oise Roy and Anne Siegel},
year = {2012},
month = mar,
type_publi = {chapitre},
x-international-audience = {no},
x-equipes = {demons PROVAL},
x-support = {diffusion},
x-type = {invitation},
topics = {team}
}
@inproceedings{bolmel13arith,
author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
title = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
booktitle = {Proceedings of the 21th IEEE Symposium on Computer Arithmetic},
address = {Austin, Texas, USA},
year = {2013},
topics = {team},
x-equipes = {demons PROVAL ext},
x-type = {article},
x-support = {actes},
x-cle-support = {ARITH},
x-international-audience = {yes},
x-proceedings = {yes},
hal = {http://hal.inria.fr/hal-00743090}
}
@inproceedings{bobot13vstte,
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
hal = {http://hal.inria.fr/hal-00875395},
title = {Preserving User Proofs Across Specification Changes},
crossref = {vstte13},
pages = {191--201},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
}
@inbook{boldo13livreim,
author = {Sylvie Boldo and Guillaume Melquiond},
hal = {http://hal-lirmm.ccsd.cnrs.fr/lirmm-00835506},
editor = {Philippe Langlois},
title = {Informatique Mathématique, une photographie en 2013},
chapter = {Arithmétique des ordinateurs et preuves formelles},
publisher = {Presses Universitaires de Perpignan},
year = {2013},
address = {Perpignan, France},
pages = {189--220},
topics = {team,lri},
type_publi = {chapitre}
}
@inproceedings{IshMelNak13,
hal = {http://hal.inria.fr/hal-00806701},
author = {Daisuke Ishii and Guillaume Melquiond and Shin Nakajima},
title = {Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus},
booktitle = {Proceedings of the 10th Conference on Integrated Formal Methods},
editor = {Einar Broch Johnsen and Luigia Petre},
address = {Turku, Finland},
year = {2013},
pages = {139--153},
series = {Lecture Notes in Computer Science},
volume = {7940},
doi = {10.1007/978-3-642-38613-8_10},
topics = {team,lri},
type_publi = {icolcomlec}
}
@article{martindorel13bit,
hal = {http://hal-ens-lyon.archives-ouvertes.fr/ensl-00644408},
topics = {team},
title = {Some Issues related to Double Roundings},
author = {Martin-Dorel, {\'E}rik and Melquiond, Guillaume and Muller, Jean-Michel},
volume = {53},
number = {4},
pages = {897--924},
journal = {BIT Numerical Mathematics},
audience = {internationale},
doi = {10.1007/s10543-013-0436-2},
year = 2013
}
@article{martindorel15jara,
topics = {team},
title = {Proving Tight Bounds on Univariate Expressions with Elementary Functions in {Coq}},
author = {Martin-Dorel, {\'E}rik and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-01086460},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
year = 2016,
doi = {10.1007/s10817-015-9350-4},
keywords = {Coq proof assistant ; formal proof ; decision procedure ; interval arithmetic ; floating-point arithmetic ; nonlinear arithmetic}
}
@inproceedings{mahboubi16itp,
topics = {team},
title = {Formally Verified Approximations of Definite Integrals},
author = {Mahboubi, Assia and Melquiond, Guillaume and Sibut-Pinote, Thomas},
hal = {https://hal.inria.fr/hal-01289616},
booktitle = {Proceedings of the 7th International Conference on Interactive Theorem Proving},
address = {Nancy, France},
editor = {Jasmin Christian Blanchette and Stephan Merz},
series = {Lecture Notes in Computer Science},
volume = {9807},
year = {2016},
month = aug,
doi = {10.1007/978-3-319-43144-4\_17},
pdf = {https://hal.inria.fr/hal-01289616/file/main.pdf},
hal_id = {hal-01289616},
hal_version = {v2}
}
@inproceedings{conchon17cav,
author = {Sylvain Conchon and Mohamed Iguernlala and Kailiang Ji and
Guillaume Melquiond and Cl\'ement Fumex},
topics = {team},
hal = {https://hal.inria.fr/hal-01522770},
title = {A Three-tier Strategy for Reasoning about
Floating-Point Numbers in {SMT}},
booktitle = {Computer Aided Verification},
year = 2017,
pages = {419--435},
series = {Lecture Notes in Computer Science},
volume = 10427,
doi = {10.1007/978-3-319-63390-9_22}
}
@inproceedings{rieuhelft17vstte,
topics = {team},
title = {How to Get an Efficient yet Verified Arbitrary-Precision Integer Library},
author = {Rieu-Helft, Rapha{\"e}l and March{\'e}, Claude and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-01519732},
booktitle = {9th Working Conference on Verified Software: Theories, Tools, and Experiments},
address = {Heidelberg, Germany},
series = {Lecture Notes in Computer Science},
volume = 10712,
year = 2017,
month = jul,
pages = {84--101},
doi = {10.1007/978-3-319-72308-2_6},
keywords = {arbitrary-precision arithmetic ; deductive program verification ; C language ; Why3 program verifier},
pdf = {https://hal.inria.fr/hal-01519732/file/main.pdf}
}
@book{boldo17,
topics = {team},
title = {Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the {Coq} System},
author = {Boldo, Sylvie and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-01632617},
publisher = {ISTE Press - Elsevier},
year = 2017,
month = dec
}
@inproceedings{melquiond18ijcar,
topics = {team},
title = {A {Why3} Framework for Reflection Proofs and its Application to {GMP}'s Algorithms},
author = {Melquiond, Guillaume and Rieu-Helft, Rapha{\"e}l},
hal = {https://hal.inria.fr/hal-01699754},
booktitle = {9th International Joint Conference on Automated Reasoning},
address = {Oxford, United Kingdom},
editor = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
series = {Lecture Notes in Computer Science},
year = 2018,
month = jul
}
@article{mahboubi19jar,
topics = {team},
title = {Formally Verified Approximations of Definite Integrals},
author = {Mahboubi, Assia and Melquiond, Guillaume and Sibut-Pinote, Thomas},
hal = {https://hal.inria.fr/hal-01630143},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = 62,
number = 2,
pages = {281--300},
year = 2019,
month = feb,
doi = {10.1007/s10817-018-9463-7}
}
@book{muller18book,
topics = {team},
title = {Handbook of Floating-point Arithmetic (2nd edition)},
author = {Muller, Jean-Michel and Brunie, Nicolas and de Dinechin, Florent and Jeannerod, Claude-Pierre and Joldes, Mioara and Lef{\`e}vre, Vincent and Melquiond, Guillaume and Revol, Nathalie and Torres, Serge},
hal = {https://hal.inria.fr/hal-01766584},
hal_local_reference = {Rapport LAAS n{\textdegree} 18106},
publisher = {Birkh{\"a}user Basel},
year = 2018,
month = jul,
doi = {10.1007/978-3-319-76526-6},
keywords = {arithmetic operators ; arithmetic algorithms ; numerical computing ; floating-point arithmetic ; computer arithmetic},
hal_id = {hal-01766584},
hal_version = {v1}
}
@phdthesis{melquiond19hdr,
topics = {team},
title = {Formal Verification for Numerical Computations, and the Other Way Around},
author = {Melquiond, Guillaume},
hal = {https://tel.archives-ouvertes.fr/tel-02194683},
school = {Universit\'e Paris Sud},
year = 2019,
month = apr,
type = {Habilitation \`a diriger des recherches}
}
@inproceedings{melquiond19jfla,
topics = {team},
title = {Computer Arithmetic and Formal Proofs},
author = {Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-02013540},
crossref = {jfla19}
}
@inproceedings{melquiond19arith,
topics = {team},
title = {Formal Verification of a State-of-the-Art Integer Square Root},
author = {Melquiond, Guillaume and Rieu-Helft, Rapha\"el},
hal = {https://hal.inria.fr/hal-02092970},
booktitle = {Symposium on Computer Arithmetic},
address = {Kyoto, Japan},
pages = {183--186},
year = 2019,
month = jun
}
@inproceedings{melquiond20issac,
topics = {team},
title = {{WhyMP}, a Formally Verified Arbitrary-Precision Integer Library},
author = {Melquiond, Guillaume and Rieu-Helft, Rapha{\"e}l},
hal = {https://hal.inria.fr/hal-02566654},
booktitle = {45th International Symposium on Symbolic and Algebraic Computation (ISSAC)},
pages = {352--359},
year = 2020,
doi = {10.1145/3373207.3404029},
keywords = {Integer arithmetic ; Deductive program verification ; Mathematical library}
}
@inproceedings{balabonski21fscd,
topics = {team},
title = {A strong call-by-need calculus},
author = {Balabonski, Thibaut and Lanco, Antoine and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-03149692},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction},
editor = {Naoki Kobayashi},
volume = 195,
pages = {9:1--9:22},
year = 2021,
doi = {10.4230/LIPIcs.FSCD.2021.9}
}
@inproceedings{boldo21arith,
topics = {team},
title = {Some Formal Tools for Computer Arithmetic: {Flocq} and {Gappa}},
author = {Boldo, Sylvie and Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-03233227},
booktitle = {28th IEEE International Symposium on Computer Arithmetic},
editor = {Mioara Joldes and Fabrizio Lamberti},
year = 2021
}
@inproceedings{melquiond21fide,
topics = {team},
title = {Plotting in a Formally Verified Way},
author = {Melquiond, Guillaume},
hal = {https://hal.inria.fr/hal-03168208},
booktitle = {6th Workshop on Formal Integrated Development Environment},
volume = 338,
pages = {39--45},
year = 2021,
doi = {10.4204/EPTCS.338.6}
}
@article{melquiond23jsc,
topics = {team},
title = {{WhyMP}, a Formally Verified Arbitrary-Precision Integer Library},
author = {Melquiond, Guillaume and Rieu-Helft, Rapha{\"e}l},
hal = {https://hal.inria.fr/hal-03233220},
journal = {Journal of Symbolic Computation},
publisher = {Elsevier},
volume = 115,
pages = {74--95},
year = 2023,
doi = {10.1016/j.jsc.2022.07.007}
}
@inproceedings{geneau23arith,
topics = {team},
author = {Geneau de Lamarli{\`e}re, Paul and Melquiond, Guillaume and Faissole, Florian},
title = {Slimmer Formal Proofs for Mathematical Libraries},
hal = {https://inria.hal.science/hal-04165169},
booktitle = {Int. Conf. on Computer Arithmetic},
year = 2023
}
@article{boldo23an,
topics = {team},
title = {Floating-point arithmetic},
author = {Boldo, Sylvie and Jeannerod, Claude-Pierre and Melquiond, Guillaume and Muller, Jean-Michel},
hal = {https://hal.science/hal-04095151},
journal = {Acta Numerica},
publisher = {Cambridge University Press},
volume = 32,
pages = {203--290},
year = 2023,
doi = {10.1017/S0962492922000101}
}
@article{martindorel23jar,
topics = {team},
title = {Enabling Floating-Point Arithmetic in the {Coq} Proof Assistant},
author = {Martin-Dorel, {\'E}rik and Melquiond, Guillaume and Roux, Pierre},
hal = {https://inria.hal.science/hal-04114233},
journal = {Journal of Automated Reasoning},
publisher = {Springer Verlag},
volume = 67,
number = 33,
year = 2023,
doi = {10.1007/s10817-023-09679-x}
}
@article{balabonski23lmcs,
topics = {team},
title = {{A strong call-by-need calculus}},
author = {Balabonski, Thibaut and Lanco, Antoine and Melquiond, Guillaume},
hal = {https://inria.hal.science/hal-03409681},
journal = {{Logical Methods in Computer Science}},
volume = 19,
number = 1,
year = 2023,
doi = {10.46298/lmcs-19(1:21)2023}
}
@proceedings{jfla12,
title = {Journ\'ees Francophones des Langages Applicatifs},
year = 2012,
booktitle = {Vingt-troisi\`emes Journ\'ees Francophones des Langages Applicatifs},
month = feb,
address = {Carnac, France},
x-international-audience = {no},
x-editorial-board = {yes},
x-proceedings = {yes},
x-cle-support = {JFLA}
}
@proceedings{jfla19,
title = {Trenti\`emes Journ\'ees Francophones des Langages Applicatifs},
booktitle = {Trenti\`emes Journ{\'e}es Francophones des Langages Applicatifs},
address = {Les Rousses, France},
year = 2019,
month = jan,
editor = {Magaud, Nicolas and Dargaye, Zaynah},
hal = {https://hal.archives-ouvertes.fr/hal-01985195v1}
}
@proceedings{smt2012,
booktitle = {SMT workshop},
editor = {Pascal Fontaine and Amit Goel},
publisher = {LORIA},
url = {http://smt2012.loria.fr/},
year = 2012,
x-international-audience = {yes},
x-proceedings = {no},
address = {Manchester, UK}
}
@proceedings{vstte13,
booktitle = {Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE)},
month = may,
year = 2013,
address = {Atherton, USA},
x-international-audience = {yes},
x-editorial-board = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {actes},
x-cle-support = {VSTTE},
editor = {Ernie Cohen and Andrey Rybalchenko},
series = {Lecture Notes in Computer Science},
volume = {8164},
publisher = {Springer}
}