boldo.bib

@comment{{This file has been generated by bib2bib 1.98}}

@comment{{Command line: /usr/bin/bib2bib -q -oc boldo.cite -ob boldo.bib -c 'author : "boldo"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}

@phdthesis{Bol04b,
  author = {Sylvie Boldo},
  title = {Preuves formelles en arithm\'etiques \`a virgule flottante},
  school = {\'Ecole Normale Sup\'erieure de Lyon},
  year = {2004},
  url = {http://www.ens-lyon.fr/LIP/Pub/Rapports/PhD/PhD2004/PhD2004-05.pdf}
}

@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{boldo15icfem,
  title = {{Formal Verification of Programs Computing the Floating-Point Average}},
  author = {Sylvie Boldo},
  hal = {https://hal.inria.fr/hal-01174892},
  booktitle = {{17th International Conference on Formal Engineering Methods}},
  address = {Paris, France},
  publisher = {{Springer}},
  year = {2015},
  month = nov,
  pdf = {https://hal.inria.fr/hal-01174892/file/article.pdf},
  topics = {team,lri},
  type_publi = {irevcomlec},
  editor = {Michael Butler and Sylvain Conchon and Fatiha Za\"idi},
  volume = {9407},
  series = {Lecture Notes in Computer Science},
  pages = {17--32}
}

@inproceedings{bol15nsv,
  author = {Sylvie Boldo},
  title = {Stupid is as Stupid Does: Taking the Square Root of the Square
    of a Floating-Point Number},
  booktitle = {Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification},
  pages = {50--55},
  year = {2015},
  editor = {Sergiy Bogomolov and Matthieu Martel},
  series = {Electronic Notes in Theoretical Computer Science},
  address = {Seattle, WA, USA},
  month = apr,
  hal = {http://hal.inria.fr/hal-01148409},
  topics = {team,lri},
  type_publi = {irevcomlec},
  doi = {http://dx.doi.org/10.1016/j.entcs.2015.10.004},
  volume = {317}
}

@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}
}

@inproceedings{boldo14scan,
  hal = {https://hal.inria.fr/hal-01088692},
  title = {Formal verification of tricky numerical computations},
  author = {Sylvie Boldo},
  year = 2014,
  booktitle = {16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics},
  address = {Würzburg, Germany},
  month = sep,
  note = {Invited talk},
  url = {http://www.scan2014.uni-wuerzburg.de/book_of_abstracts/},
  topics = {team,lri},
  type_publi = {colloque}
}

@article{boldo14larecherche,
  hal = {http://hal.inria.fr/ensl-01069744},
  author = {Sylvie Boldo and Jean-Michel Muller},
  title = {Des ordinateurs capables de calculer plus juste},
  journal = {La Recherche},
  year = {2014},
  volume = {492},
  pages = {46--52},
  month = oct,
  topics = {team,lri},
  type_publi = {diffusion}
}

@incollection{boldo14breves,
  title = {{M{\^e}me les ordinateurs font des erreurs !}},
  author = {Boldo, Sylvie},
  hal = {https://hal.inria.fr/hal-01089095},
  booktitle = {{Br{\`e}ves de maths}},
  editor = {Martin Andler and Liliane Bel and Sylvie Benzoni-Gavage and Thierry Goudon and Cyril Imbert and Antoine Rousseau},
  publisher = {{Nouveau Monde Editions}},
  pages = {136-137},
  year = {2014},
  month = oct,
  url = {http://mpt2013.fr/meme-les-ordinateurs-font-des-erreurs/},
  topics = {team,lri},
  type_publi = {diffusion}
}

@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}
}

@inproceedings{Bol06,
  author = {Sylvie Boldo},
  title = {Pitfalls of a full floating-point proof: example on the formal proof of the {Veltkamp/Dekker} algorithms},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  pages = {52-66},
  x-pdf = {http://www.lri.fr/~sboldo/files/ijcar06.pdf},
  url = {http://www.lri.fr/~sboldo/files/ijcar06.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {IJCAR},
  crossref = {ijcar06}
}

@inproceedings{BolMun06,
  author = {Sylvie Boldo and C\'esar Mu{\~n}oz},
  title = {Provably Faithful Evaluation of Polynomials},
  booktitle = {Proceedings of the 21st Annual ACM Symposium on Applied Computing},
  year = {2006},
  month = apr,
  address = {Dijon, France},
  topics = {team},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  volume = 2,
  hal = {http://hal.inria.fr/inria-00050232/en/},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {SAC},
  pages = {1328-1332}
}

@inproceedings{BoldoFilliatre07,
  author = {Sylvie Boldo and Jean-Christophe Filli\^atre},
  doi = {10.1109/ARITH.2007.20},
  title = {Formal Verification of Floating-Point Programs},
  booktitle = {18th IEEE International Symposium on Computer Arithmetic},
  pages = {187--194},
  x-month = jun,
  year = 2007,
  x-address = {Montpellier, France},
  topics = {team,lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/caduceus-floats.pdf},
  url = {https://usr.lmf.cnrs.fr/~jcf/publis/caduceus-floats.pdf},
  abstract = {
  This paper introduces a methodology to perform formal verification
  of floating-point C programs. It extends an existing tool for the
  verification of C programs, Caduceus, with new annotations specific
  to floating-point arithmetic. The Caduceus first-order logic model
  for C programs is extended accordingly. Then verification conditions
  expressing the correctness of the programs are obtained in the usual
  way and can be discharged interactively with the Coq proof
  assistant, using an existing Coq formalization of floating-point
  arithmetic.  This methodology is already implemented and has been
  successfully applied to several short floating-point programs, which
  are presented in this paper.}
}

@article{bol08tc2,
  author = {Sylvie Boldo and Marc Daumas and Ren-Cang Li},
  title = {Formally Verified Argument Reduction with a Fused-Multiply-Add},
  journal = {IEEE Transactions on Computers},
  year = {2009},
  volume = {58},
  number = {8},
  issn = {0018-9340},
  pages = {1139-1145},
  doi = {10.1109/TC.2008.216},
  publisher = {IEEE Computer Society},
  address = {Los Alamitos, CA, USA},
  url = {http://arxiv.org/abs/0708.3722},
  topics = {team,lri},
  type_publi = {irevcomlec},
  type_digiteo = {revue_cl},
  x-pdf = {http://arxiv.org/pdf/0708.3722v1},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {ITComputers},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-pays = {US}
}

@article{Bol09tc,
  author = {Sylvie Boldo},
  title = {{K}ahan's algorithm for a correct discriminant computation at last formally proven},
  journal = {IEEE Transactions on Computers},
  month = feb,
  url = {http://hal.inria.fr/inria-00171497/},
  volume = {58},
  number = {2},
  issn = {0018-9340},
  year = {2009},
  pages = {220-225},
  doi = {10.1109/TC.2008.200},
  publisher = {IEEE Computer Society},
  address = {Los Alamitos, CA, USA}
}

@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{bol08rnc,
  title = {Formal proof for delayed finite field arithmetic using floating point operators},
  author = {Sylvie Boldo and Marc Daumas and Pascal Giorgi},
  booktitle = {Proceedings of the 8th Conference on Real Numbers and
                   Computers},
  year = {2008},
  address = {Santiago de Compostela, Spain},
  month = jul,
  pages = {113--122},
  editor = {Daumas, Marc and Bruguera, Javier},
  x-pdf = {http://hal.archives-ouvertes.fr/docs/00/27/89/89/PDF/rnc.pdf},
  hal = {http://hal.inria.fr/inria-00278989/en/},
  topics = {team,lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {RNC},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}

@inproceedings{bol05arith,
  author = {Sylvie Boldo and Jean-Michel Muller},
  title = {Some Functions Computable with a Fused-mac},
  year = 2005,
  address = {Cape Cod, USA},
  booktitle = {Proceedings of the 17th Symposium on Computer Arithmetic},
  url = {http://perso.ens-lyon.fr/jean-michel.muller/FmacArith.pdf},
  editor = {Montuschi, Paolo and Schwarz, Eric},
  pages = {52-58},
  topics = {team,lri},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  type_publi = {icolcomlec}
}

@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}
}

@incollection{boldodiffusion08,
  author = {Sylvie Boldo},
  title = {Demandez le programme!},
  booktitle = {DocSciences},
  pages = {26--33},
  publisher = {C.R.D.P. de l'acad\'emie de Versailles},
  year = {2008},
  volume = {5},
  month = nov,
  topics = {team, lri},
  url = {http://www.docsciences.fr/-DocSciences-no5-},
  note = {\url{http://www.docsciences.fr/-DocSciences-no5-}},
  type_publi = {diffusion},
  x-scientific-popularization = {yes}
}

@misc{boldo09diffusion,
  author = {Sylvie Boldo},
  title = {Demandez le programme!},
  howpublished = {Interstices},
  year = {2009},
  month = feb,
  topics = {team, lri},
  url = {http://interstices.info/demandez-le-programme},
  note = {\url{http://interstices.info/demandez-le-programme}},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {diffusion},
  x-scientific-popularization = {yes}
}

@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}
}

@inproceedings{boldo09icalp,
  author = {Sylvie Boldo},
  title = {Floats and Ropes: A Case Study for Formal Numerical Program Verification},
  booktitle = {36th International Colloquium on Automata, Languages and Programming},
  pages = {91--102},
  year = {2009},
  volume = {5556},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-support = {actes},
  topics = {team},
  doi = {10.1007/978-3-642-02930-1_8},
  x-url = {http://fost.saclay.inria.fr/files/icalp2009trackb_submission_48.pdf}
}

@article{boldo10-tc,
  title = {Exact and {A}pproximated error of the {FMA}},
  author = {Boldo, Sylvie and Muller, Jean-Michel},
  abstract = {The fused multiply accumulate-add (FMA) instruction,
                  specified by the IEEE 754-2008 Standard for
                  Floating-Point Arithmetic, eases some calculations,
                  and is already available on some current processors
                  such as the Power PC or the Itanium. We first extend
                  an earlier work on the computation of the exact
                  error of an FMA (by giving more general conditions
                  and providing a formal proof). Then, we present a
                  new algorithm that computes an approximation to the
                  error of an FMA, and provide error bounds and a
                  formal proof for that algorithm.},
  journal = {IEEE Transactions on Computers},
  publisher = {IEEE Computer Society},
  address = {Los Alamitos, CA, USA},
  year = {2011},
  month = feb,
  volume = {60},
  number = {2},
  pages = {157--164},
  hal = {http://hal.inria.fr/inria-00429617/en/},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-support = {diffusion},
  x-type = {article}
}

@misc{boldo10diffusion,
  author = {Sylvie Boldo},
  title = {C'est la faute \`a l'ordinateur!},
  howpublished = {Interstices -- Id\'ee re\c{c}ue},
  year = {2010},
  month = feb,
  topics = {team, lri},
  note = {\url{http://interstices.info/idee-recue-informatique-18}},
  web = {http://interstices.info/idee-recue-informatique-18},
  hal = {http://hal.inria.fr/inria-00534848/fr/},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {diffusion},
  x-scientific-popularization = {yes}
}

@inproceedings{boldo10-nfm,
  author = {Sylvie Boldo and Nguyen, Thi Minh Tuyen},
  title = {Hardware-independent proofs of numerical programs},
  booktitle = {Proceedings of the Second NASA Formal Methods Symposium},
  year = 2010,
  series = {NASA Conference Publication},
  address = {Washington D.C., USA},
  month = apr,
  x-equipes = {demons PROVAL},
  x-support = {actes},
  x-cle-support = {NASAFM},
  x-type = {article},
  topics = {team},
  pages = {14--23},
  editor = {C\'esar Mu{\~n}oz},
  hal = {http://hal.inria.fr/inria-00534410/en/},
  x-pdf = {http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-editorial-board = {yes}
}

@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}
}

@inproceedings{boldo10-nsv,
  author = {Sylvie Boldo},
  title = {{Formal verification of numerical programs: from C annotated programs to Coq proofs}},
  booktitle = {Proceedings of the Third International Workshop on Numerical Software Verification},
  address = {Edinburgh, Scotland},
  year = {2010},
  month = jul,
  x-international-audience = {yes},
  x-invited-conference = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  note = {NSV-8},
  annote = {Invited paper},
  x-equipes = {demons PROVAL},
  x-support = {actes_aux},
  x-cle-support = {NSV},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/inria-00534400/en/}
}

@misc{boldo10-webtv,
  author = {Sylvie Boldo},
  x-equipes = {demons PROVAL},
  x-support = {video},
  x-type = {vulgarisation},
  topics = {team},
  title = {L'informatique},
  web = {http://www.universcience.tv/media/1340/l-informatique.html},
  note = {Quiz 5-12, \url{http://www.universcience.tv/media/1340/l-informatique.html}},
  hal = {http://hal.inria.fr/inria-00534852/fr/},
  month = apr,
  year = 2010,
  howpublished = {Universcience web television},
  x-scientific-popularization = {yes}
}

@misc{nguyen10poster,
  author = {Nguyen, Thi Minh Tuyen  and Boldo, Sylvie and March\'e, Claude},
  title = {Formal proofs of numerical programs},
  howpublished = {Poster at the Digiteo Forum, Palaiseau, France},
  month = oct,
  year = 2010,
  x-scientific-popularization = {yes},
  hal = {http://hal.inria.fr/inria-00536135/en/}
}

@article{boldo11-isse,
  author = {Sylvie Boldo and Thi Minh Tuyen Nguyen},
  title = {Proofs of numerical programs when the compiler optimizes},
  journal = {Innovations in Systems and Software Engineering},
  year = {2011},
  pages = {151--160},
  volume = {7},
  issue = {2},
  hal = {http://hal.inria.fr/hal-00777639},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  topics = {team},
  x-support = {revue},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-cle-support = {ISSE}
}

@misc{boldo08diffusion-2,
  author = {Sylvie Boldo and Thierry Vi\'eville},
  title = {L'informatique, ce n'est pas pour les filles},
  howpublished = {Interstices},
  year = {2008},
  topics = {team},
  month = sep,
  url = {http://interstices.info/idee-recue-informatique-5},
  note = {\url{http://interstices.info/idee-recue-informatique-5}},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {diffusion},
  x-scientific-popularization = {yes}
}

@misc{boldo10diffusion-2,
  author = {Sylvie Boldo},
  title = {Un algorithme de d\'ecoupe de g\^ateau},
  howpublished = {Interstices},
  year = {2010},
  topics = {team},
  month = jul,
  url = {http://interstices.info/decoupe},
  note = {\url{http://interstices.info/decoupe}},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {diffusion},
  x-scientific-popularization = {yes}
}

@misc{boldopodcast08,
  author = {Sylvie Boldo},
  title = {Pourquoi mon ordinateur calcule-t-il faux?},
  howpublished = {Interstices},
  year = {2008},
  month = apr,
  topics = {team},
  note = {Podcast, \url{http://interstices.info/a-propos-calcul-ordinateurs}},
  url = {http://interstices.info/a-propos-calcul-ordinateurs},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {diffusion},
  x-scientific-popularization = {yes}
}

@article{boldo11mcs,
  author = {Sylvie Boldo and Claude March\'e},
  title = {Formal verification of numerical programs: from {C} annotated programs to mechanical proofs},
  journal = {Mathematics in Computer Science},
  topics = {team},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {MCS},
  x-equipes = {demons PROVAL},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  year = 2011,
  publisher = {Birkhauser Basel},
  issn = {1661-8270},
  pages = {377--393},
  volume = {5},
  issue = {4},
  doi = {10.1007/s11786-011-0099-9},
  hal = {http://hal.inria.fr/hal-00777605}
}

@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}
}

@incollection{Boldo11livrea,
  author = {Sylvie Boldo and Thierry Vi\'eville},
  editor = {Gilles Dowek},
  title = {Repr\'esentation num\'erique de l'information},
  booktitle = {Introduction \`a la science informatique},
  pages = {23--72},
  publisher = {CRDP Acad\'emie de Paris},
  year = {2011},
  url = {http://crdp.ac-paris.fr/Introduction-a-la-science},
  series = {Rep\`eres pour agir},
  month = jul,
  isbn = {2866311884},
  x-equipes = {demons PROVAL},
  x-type = {chapitre},
  x-support = {ouvrage},
  topics = {team}
}

@incollection{Boldo11livreb,
  author = {Sylvie Boldo and Thierry Vi\'eville},
  editor = {Gilles Dowek},
  title = {Structuration et contr\^ole de l'information},
  booktitle = {Introduction \`a la science informatique},
  pages = {281--308},
  publisher = {CRDP Acad\'emie de Paris},
  year = {2011},
  url = {http://crdp.ac-paris.fr/Introduction-a-la-science},
  series = {Rep\`eres pour agir},
  month = jul,
  isbn = {2866311884},
  x-equipes = {demons PROVAL},
  x-type = {chapitre},
  x-support = {ouvrage},
  topics = {team}
}

@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}
}

@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}
}

@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{boldo13arith,
  author = {Sylvie Boldo},
  title = {How to Compute the Area of a Triangle: a Formal Revisit},
  booktitle = {Proceedings of the 21th IEEE Symposium on Computer Arithmetic},
  address = {Austin, Texas, USA},
  year = {2013},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-international-audience = {yes},
  x-proceedings = {yes},
  hal = {http://hal.inria.fr/hal-00790071}
}

@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}
}

@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}
}

@techreport{rousseau13,
  hal = {http://hal.inria.fr/hal-00804915},
  topics = {team},
  hal_id = {hal-00804915},
  url = {http://hal.inria.fr/hal-00804915},
  title = {M{\'e}diation Scientifique : une facette de nos m{\'e}tiers de la recherche},
  author = {Rousseau, Antoine and Darnaud, Aur{\'e}lie and Goglin, Brice and Acharian, C{\'e}line and Leininger, Christine and Godin, Christophe and Holik, Clarisse and Kirchner, Claude and Rives, Diane and Darquie, Elodie and Kerrien, Erwan and Neyret, Fabrice and Masseglia, Florent and Dufour, Florian and Berry, G{\'e}rard and Dowek, Gilles and Robak, H{\'e}l{\`e}ne and Xypas, H{\'e}l{\`e}ne and Illina, Irina and Gnaedig, Isabelle and Jongwane, Joanna and Ehrel, Jocelyne and Viennot, Laurent and Guion, Laure and Calderan, Lisette and Kovacic, Lola and Collin, Marie and Enard, Marie-Agn{\`e}s and Comte, Marie-H{\'e}l{\`e}ne and Quinson, Martin and Olivi, Martine and Giraud, Mathieu and Dor{\'e}mus, Mathilde and Ogouchi, Mia and Droin, Muriel and Lacaux, Nathalie and Rougier, Nicolas and Roussel, Nicolas and Guitton, Pascal and Peterlongo, Pierre and Cornus, Rose-Marie and Vandermeersch, Simon and Maheo, Sophie and Lefebvre, Sylvain and Boldo, Sylvie and Vi{\'e}ville, Thierry and Poirel, V{\'e}ronique and Chabreuil, Aline and Fischer, Arnaud and Farge, Claude and Vadel, Claude and Astic, Isabelle and Dumont, Jean-Pierre and F{\'e}joz, Loic and Rambert, Patrick and Paradinas, Pierre and De Quatrebarbes, Sophie and Laurent, St{\'e}phane},
  abstract = {Dans ce monde devenu num{\'e}rique nous savons que c'est une de nos missions d'acteur de la recherche publique, que de rendre accessibles les sciences du num{\'e}rique au plus grand nombre. Ceci afin que chaque citoyenne et citoyen ma{\^\i}trise, au del{\`a} des usages, les principaux fondements de cette mutation num{\'e}rique. Et nous croyons que c'est l'acquisition d'une culture scientifique sur ces sujets qui est le levier de cette appropriation. C'est notre mission et notre plaisir d'y contribuer. Ce document a pour but d'aider chaque coll{\`e}gue Inria int{\'e}ress{\'e} {\`a} participer {\`a} ce volet de nos missions. Devenue une facette de notre m{\'e}tier, comme le rappelle le Plan Strat{\'e}gique Inria [1], ce que nous appelons m{\'e}diation scientifique en sciences du num{\'e}rique (alias, " mecsci ") se professionnalise et change d'{\'e}chelle. Et c'est environ 1 \% de nos ressources qui a vocation {\`a} y {\^e}tre consacr{\'e}. Pour tout l'institut on parle donc de pr{\`e}s de 40 {\'e}quivalents temps-plein distribu{\'e}s {\`a} travers le travail quotidien ou ponctuel de plusieurs centaines de coll{\`e}gues chercheurs, ing{\'e}nieurs, communicants, etc.. Une telle {\'e}nergie m{\'e}rite d'{\^e}tre bien employ{\'e}e : au service des meilleurs objectifs ; vers des cibles bien d{\'e}finies qui ont de vrais besoins sur ces sujets ; dans le cadre d'actions leviers qui aident {\`a} faire bouger les choses ; et avec une m{\'e}thodologie efficace qui optimise ce que nous investissons dans de telles activit{\'e}s ; tout en respectant et en encourageant les dynamiques locales et individuelles ind{\'e}pendantes qui restent les sources vives de la m{\'e}diation scientifique. Voil{\`a} pourquoi il y a juste besoin d'offrir en partage {\`a} chacune et chacun les {\'e}l{\'e}ments fondateurs et m{\'e}thodologiques de cette m{\'e}diation scientifique. Offrir aussi quelques bonnes pratiques tr{\`e}s concr{\`e}tes. On parle donc ici d'une organisation distribu{\'e}e d'actions collaboratives d'o{\`u} {\'e}merge le service public de popularisation scientifique vis{\'e}. C'est ce que ce document se propose de d{\'e}crire ici.},
  keywords = {m{\'e}diation scientifique ; culture scientifique ; recherche ; popularisation des sciences ; service public.},
  language = {Fran\c{c}ais},
  affiliation = {MOISE - INRIA Grenoble Rh{\^o}ne-Alpes / LJK Laboratoire Jean Kuntzmann , INRIA Paris-Rocquencourt - INRIA , RUNTIME - INRIA Bordeaux - Sud-Ouest , Laboratoire Bordelais de Recherche en Informatique - LaBRI , INRIA Si{\`e}ge - INRIA , Virtual Plants - VP , UMR Am{\'e}lioration G{\'e}n{\'e}tique et Adaptation des Plantes M{\'e}diterran{\'e}eennes et Tropicales - AGAP , PAREO - INRIA Lorraine - LORIA , MAGRIT - INRIA Nancy - Grand Est / LORIA , MAVERICK - Inria Grenoble Rh{\^o}ne-Alpes / LJK Laboratoire Jean Kuntzmann , Laboratoire d'Informatique de Robotique et de Micro{\'e}lectronique de Montpellier - LIRMM , ZENITH - INRIA Sophia Antipolis , INRIA Sophia Antipolis - INRIA Sophia Antipolis , DEDUCTEAM - INRIA Paris-Rocquencourt , PAROLE - INRIA Nancy - Grand Est / LORIA , CARTE - INRIA Nancy - Grand Est / LORIA , GANG - INRIA Rocquencourt , Laboratoire d'informatique Algorithmique : Fondements et Applications - LIAFA , Laboratory of Information, Network and Communication Sciences - LINCS , Service IST Sophia Antipolis M{\'e}diterran{\'e}e / Laboratoire I3S - INRIA Sophia Antipolis - M{\'e}diterran{\'e}e , ALGORILLE - INRIA Nancy - Grand Est / LORIA , APICS - INRIA Sophia Antipolis , Laboratoire d'Informatique Fondamentale de Lille - LIFL , BONSAI - INRIA Lille - Nord Europe , FUSCIA - INRIA , CORTEX - INRIA Lorraine - LORIA , MINT - INRIA Lille - Nord Europe , GENSCALE - INRIA - IRISA , ALICE - INRIA Nancy - Grand Est / LORIA , Laboratoire de Recherche en Informatique - LRI , TOCCATA - INRIA Saclay - {\^I}le-de-France , Mnemosyne - INRIA Bordeaux - Sud-Ouest , MADYNES - INRIA Lorraine - LORIA , MOSEL - INRIA Lorraine - LORIA , Centre for Quantitative methods and Operations Management - QuantOM},
  pages = 34,
  type = {Interne},
  institution = {Inria},
  year = 2013,
  month = mar
}

@phdthesis{boldo14hdr,
  hal = {https://hal.inria.fr/tel-01089643},
  author = {Sylvie Boldo},
  title = {Deductive Formal Verification: How To Make Your Floating-Point Programs Behave},
  year = 2014,
  month = oct,
  type = {Th\`{e}se d'habilitation},
  school = {Universit{\'e} Paris-Sud},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {habilitation},
  x-support = {rapport},
  topics = {team}
}

@inproceedings{boldo16nsv,
  title = {{Computing a correct and tight rounding error bound using
                  rounding-to-nearest}},
  author = {Boldo, Sylvie},
  hal = {https://hal.inria.fr/hal-01377152},
  booktitle = {{9th International Workshop on Numerical Software Verification}},
  address = {Toronto, Canada},
  year = {2016},
  month = jul,
  pdf = {https://hal.inria.fr/hal-01377152/file/article.pdf},
  topics = {team}
}

@inproceedings{boldo16hccv,
  title = {{Iterators: where folds fail}},
  author = {Boldo, Sylvie},
  hal = {https://hal.inria.fr/hal-01377155},
  booktitle = {{Workshop on High-Consequence Control Verification}},
  address = {Toronto, Canada},
  year = {2016},
  month = jul,
  pdf = {https://hal.inria.fr/hal-01377155/file/abstract.pdf},
  topics = {team}
}

@misc{vieville:hal-01238442,
  topics = {team},
  title = {{ Structures : organisation, complexit\'e, dynamique des mot-cl\'es
                  au sens inattendu}},
  author = {Vieville, Thierry and Boldo, Sylvie and Masseglia, Florent and
                  Bernhard, Pierre},
  year = {2015},
  month = apr,
  hal = {https://hal.inria.fr/hal-01238442},
  note = {Article de vulgarisation sur pixees.fr},
  hal_id = {hal-01238442},
  hal_version = {v1},
  x-scientific-popularization = {yes}
}

@inproceedings{boldo:hal-01391578,
  topics = {team},
  title = {{A Coq Formal Proof of the Lax-Milgram theorem}},
  author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian
                  and Martin, Vincent and Mayero, Micaela},
  hal = {https://hal.inria.fr/hal-01391578},
  booktitle = {{Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}},
  series = {CPP 2017},
  location = {Paris, France},
  year = {2017},
  month = jan,
  pages = {79--89},
  pdf = {https://hal.inria.fr/hal-01391578/file/article.pdf},
  doi = {10.1145/3018610.3018625},
  publisher = {ACM},
  address = {New York, NY, USA}
}

@article{boldo17toms,
  topics = {team},
  title = {On the robustness of the {2Sum} and {Fast2Sum} algorithms},
  author = {Boldo, Sylvie and Graillat, Stef and Muller, Jean-Michel},
  hal = {https://hal-ens-lyon.archives-ouvertes.fr/ensl-01310023},
  journal = {ACM Transactions on Mathematical Software},
  publisher = {ACM Press},
  year = {2017},
  volume = {44},
  number = {1},
  month = jul,
  pdf = {https://hal-ens-lyon.archives-ouvertes.fr/ensl-01310023/file/FaithfulTwoSum-Final-Fev2017.pdf}
}

@inproceedings{boldo17arith,
  topics = {team},
  title = {Round-off Error Analysis of Explicit One-Step Numerical Integration Methods},
  author = {Boldo, Sylvie and Faissole, Florian and Chapoutot, Alexandre},
  hal = {https://hal.archives-ouvertes.fr/hal-01581794},
  booktitle = {24th IEEE Symposium on Computer Arithmetic},
  address = {London, United Kingdom},
  year = {2017},
  month = jul,
  doi = {10.1109/ARITH.2017.22},
  pdf = {https://hal.archives-ouvertes.fr/hal-01581794/file/arith_hal.pdf}
}

@inproceedings{boldo17itp,
  topics = {team},
  title = {Formal Verification of a Floating-Point Expansion Renormalization Algorithm},
  author = {Boldo, Sylvie and Joldes, Mioara and Muller, Jean-Michel and Popescu, Valentina},
  hal = {https://hal.archives-ouvertes.fr/hal-01512417},
  year = {2017},
  month = sep,
  pdf = {https://hal.archives-ouvertes.fr/hal-01512417/file/itp17.pdf},
  booktitle = {Proceedings of the 8th International Conference on Interactive Theorem Proving},
  address = {Brasilia, Brazil}
}

@inproceedings{BCF17b,
  topics = {team},
  title = {Preuve formelle du th{\'e}or{\`e}me de {Lax--Milgram}},
  author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
  hal = {https://hal.archives-ouvertes.fr/hal-01581807},
  booktitle = {{16{\`e}mes journ{\'e}es Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels}},
  address = {Montpellier, France},
  year = {2017},
  month = jun,
  pdf = {https://hal.archives-ouvertes.fr/hal-01581807/file/article_afadl.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{boldo18arith,
  topics = {team},
  title = {A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers},
  author = {Boldo, Sylvie and Faissole, Florian and Tourneur, Vincent},
  hal = {https://hal.inria.fr/hal-01772272},
  booktitle = {25th IEEE Symposium on Computer Arithmetic},
  address = {Amherst, MA, United States},
  year = 2018,
  month = jun
}

@unpublished{galloiswong18calculemus,
  topics = {team},
  title = {{A Coq formalization of digital filters}},
  author = {Gallois-Wong, Diane and Boldo, Sylvie and Hilaire, Thibault},
  hal = {https://hal.inria.fr/hal-01728828},
  booktitle = {{CICM 2018 - 11th Conference on Intelligent Computer Mathematics}},
  address = {Hagenberg, Austria},
  editor = {Florian Rabe and William M. Farmer and Grant O. Passmore and Abdou Youssef},
  series = {Intelligent Computer Mathematics},
  pages = {87--103},
  year = {2018},
  month = aug,
  doi = {10.1007/978-3-319-96812-4\_8},
  pdf = {https://hal.inria.fr/hal-01728828/file/CICM18.pdf}
}

@article{galloiswong19na,
  topics = {team},
  title = {Optimal Inverse Projection of Floating-Point Addition},
  author = {Gallois-Wong, Diane and Boldo, Sylvie and Cuoq, Pascal},
  hal = {https://hal.inria.fr/hal-01939097},
  journal = {Numerical Algorithms},
  publisher = {Springer},
  year = 2019,
  doi = {10.1007/s11075-019-00711-z},
  pdf = {https://hal.inria.fr/hal-01939097/file/main.pdf}
}

@article{boldo19toc,
  topics = {team},
  title = {Round-off error and exceptional behavior analysis of explicit {Runge-Kutta} methods},
  author = {Boldo, Sylvie and Faissole, Florian and Chapoutot, Alexandre},
  hal = {https://hal.archives-ouvertes.fr/hal-01883843},
  journal = {IEEE Transactions on Computers},
  publisher = {Institute of Electrical and Electronics Engineers},
  year = 2019,
  doi = {10.1109/TC.2019.2917902},
  pdf = {https://hal.archives-ouvertes.fr/hal-01883843/file/article_hal.pdf}
}

@unpublished{boldo19wp,
  topics = {team},
  title = {Emulating round-to-nearest-ties-to-zero ''augmented'' floating-point operations using round-to-nearest-ties-to-even arithmetic},
  author = {Boldo, Sylvie and Lauter, Christoph Q. and Muller, Jean-Michel},
  hal = {https://hal.archives-ouvertes.fr/hal-02137968},
  note = {working paper or preprint},
  year = 2019,
  month = oct
}

@techreport{boldo21rr,
  topics = {team},
  title = {A {Coq} Formalization of {Lebesgue} Integration of Nonnegative Functions},
  author = {Boldo, Sylvie and Cl{\'e}ment, Fran\c{c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
  hal = {https://hal.inria.fr/hal-03194113},
  type = {Research Report},
  number = {RR-9401},
  institution = {Inria, France},
  year = 2021,
  keywords = {Lebesgue integration ; Measure theory ; Coq ; Formal proof ; Coq ; Preuve formelle ; Th{\'e}orie de la mesure ; Int{\'e}grale de Lebesgue}
}

@article{galloiswong20na,
  topics = {team},
  title = {Optimal Inverse Projection of Floating-Point Addition},
  author = {Gallois-Wong, Diane and Boldo, Sylvie and Cuoq, Pascal},
  hal = {https://hal.inria.fr/hal-01939097},
  journal = {Numerical Algorithms},
  publisher = {Springer},
  volume = 83,
  number = 3,
  pages = {957--986},
  year = 2020,
  doi = {10.1007/s11075-019-00711-z}
}

@article{boldo20tc,
  topics = {team},
  title = {Emulating round-to-nearest ties-to-zero ''augmented'' floating-point operations using round-to-nearest ties-to-even arithmetic},
  author = {Boldo, Sylvie and Lauter, Christoph Q. and Muller, Jean-Michel},
  hal = {https://hal.archives-ouvertes.fr/hal-02137968},
  journal = {Transactions on Computers},
  publisher = {{IEEE} Comp. Soc. Press},
  year = 2020,
  doi = {10.1109/TC.2020.3002702},
  keywords = {Numerical reproducibility ; Floating-point arithmetic ; Numerical repro- ducibility ; Formal proof ; Rounding mode ; Error-free transforms ; Rounding error analysis}
}

@inproceedings{boldo20arith,
  topics = {team},
  title = {A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm},
  author = {Boldo, Sylvie and Gallois-Wong, Diane and Hilaire, Thibault},
  hal = {https://hal.inria.fr/hal-02982017},
  booktitle = {27th IEEE Symposium on Computer Arithmetic (ARITH)},
  publisher = {IEEE},
  pages = {9--16},
  year = 2020,
  doi = {10.1109/ARITH48897.2020.00011},
  keywords = {Dot Product ; Sum-of-Products ; Correct Round- ing ; Odd Rounding ; Fixed-Point Arithmetic}
}

@article{boldo21toc,
  topics = {team},
  title = {Emulating round-to-nearest ties-to-zero ''augmented'' floating-point operations using round-to-nearest ties-to-even arithmetic},
  author = {Boldo, Sylvie and Lauter, Christoph Q. and Muller, Jean-Michel},
  hal = {https://hal.archives-ouvertes.fr/hal-02137968},
  journal = {IEEE Transactions on Computers},
  volume = 70,
  number = 7,
  pages = {1046--1058},
  year = 2021,
  doi = {10.1109/TC.2020.3002702}
}

@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
}

@article{bensalemknapp22tetc,
  topics = {team},
  title = {Bounding the Round-Off Error of the Upwind Scheme for Advection},
  author = {Ben Salem-Knapp, Louise and Boldo, Sylvie and Weens, William},
  hal = {https://hal.inria.fr/hal-03329933},
  journal = {IEEE Transactions on Emerging Topics in Computing},
  publisher = {IEEE},
  volume = 10,
  number = 3,
  year = 2022,
  doi = {10.1109/TETC.2022.3191472},
  keywords = {Round-off error ; Floating-Point ; Numerical Scheme ; Advection ; Hydrodynamics}
}

@unpublished{boldo22,
  topics = {team},
  title = {A {Coq} Formalization of the {Bochner} integral},
  author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Leclerc, Louise},
  hal = {https://hal.inria.fr/hal-03516749},
  note = {working paper or preprint},
  year = 2022
}

@article{boldo22jar,
  topics = {team},
  title = {A {Coq} Formalization of {Lebesgue} Integration of Nonnegative Functions},
  author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Faissole, Florian and Martin, Vincent and Mayero, Micaela},
  hal = {https://hal.inria.fr/hal-03471095},
  journal = {Journal of Automated Reasoning},
  publisher = {Springer},
  volume = 66,
  pages = {175--213},
  year = 2022,
  doi = {10.1007/s10817-021-09612-0}
}

@inproceedings{boldo23fm,
  topics = {team},
  title = {A {Coq} Formalization of {Lebesgue} Induction Principle and {Tonelli's} Theorem},
  author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Martin, Vincent and Mayero, Micaela and Mouhcine, Houda},
  hal = {https://hal.inria.fr/hal-03889276},
  booktitle = {25th International Symposium on Formal Methods (FM 2023)},
  series = {Lecture Notes in Computer Science},
  volume = 14000,
  pages = {39--55},
  year = 2023,
  doi = {10.1007/978-3-031-27481-7\_4}
}

@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}
}

@techreport{boldo23rr,
  topics = {team},
  title = {{Lebesgue} Induction and {Tonelli}'s Theorem in {Coq}},
  author = {Boldo, Sylvie and Cl{\'e}ment, Fran{\c c}ois and Martin, Vincent and Mayero, Micaela and Mouhcine, Houda},
  hal = {https://inria.hal.science/hal-03564379},
  type = {Research Report},
  number = 9457,
  institution = {Inria},
  year = 2023
}

@proceedings{ijcar06,
  title = {International Joint Conference on Automated Reasoning},
  booktitle = {Third International Joint Conference on Automated Reasoning},
  editor = {Ulrich Furbach and Natarajan Shankar},
  year = 2006,
  series = {Lecture Notes in Computer Science},
  volume = 4130,
  address = {Seattle, USA},
  month = aug,
  publisher = {Springer}
}