Publications of Sylvie Boldo

boldo_ref.bib

@article{BLM20,
  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},
  url = {https://hal.archives-ouvertes.fr/hal-02137968},
  journal = {{IEEE Transactions on Computers}},
  note = {Accepted for publication},
  year = {2020},
  month = jun,
  pdf = {https://hal.archives-ouvertes.fr/hal-02137968/file/Emulation-RN0-revised.pdf},
  hal_id = {hal-02137968},
  hal_version = {v4}
}
@inproceedings{BGWH20,
  author = {Boldo, Sylvie and Gallois-Wong, Diane and Hilaire, Thibault},
  title = {{A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm}},
  booktitle = {Proceedings of the 27th Symposium on Computer Arithmetic (ARITH 2020)},
  year = {2020},
  month = jun,
  address = {Portland, Oregon},
  publisher = {{IEEE}}
}
@proceedings{BL19,
  title = {{Proceedings of the 26th Symposium on Computer Arithmetic (ARITH 2019)}},
  author = {Boldo, Sylvie and Langhammer, Martin},
  url = {https://hal.inria.fr/hal-02433652},
  booktitle = {{ARITH 2019 - 26th IEEE Symposium on Computer Arithmetic}},
  address = {Kyoto},
  publisher = {{IEEE}},
  year = {2019},
  month = jun,
  doi = {10.1109/ARITH.2019.00005},
  hal_id = {hal-02433652},
  hal_version = {v1}
}
@article{BFC19,
  title = {{Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods}},
  author = {Boldo, Sylvie and Faissole, Florian and Chapoutot, Alexandre},
  url = {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}
}
@article{GWBC20,
  title = {{Optimal Inverse Projection of Floating-Point Addition}},
  author = {Gallois-Wong, Diane and Boldo, Sylvie and Cuoq, Pascal},
  url = {https://hal.inria.fr/hal-01939097},
  journal = {{Numerical Algorithms}},
  publisher = {{Springer Verlag}},
  volume = {83},
  number = {3},
  pages = {957--986},
  year = {2020},
  doi = {10.1007/s11075-019-00711-z},
  pdf = {https://hal.inria.fr/hal-01939097/file/main.pdf},
  hal_id = {hal-01939097},
  hal_version = {v1}
}
@inproceedings{GWBH18,
  title = {{A Coq formalization of digital filters}},
  author = {Gallois-Wong, Diane and Boldo, Sylvie and Hilaire, Thibault},
  url = {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},
  hal_id = {hal-01728828},
  hal_version = {v2}
}
@inproceedings{BFT18,
  title = {A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers},
  author = {Boldo, Sylvie and Faissole, Florian and Tourneur, Vincent},
  url = {https://hal.inria.fr/hal-01772272},
  booktitle = {25th IEEE Symposium on Computer Arithmetic},
  address = {Amherst, MA, United States},
  year = 2018,
  month = jun,
  doi = {10.1109/ARITH.2018.8464761}
}
@proceedings{BM18,
  title = {{Journ{\'e}es Francophones des Langages Applicatifs 2018}},
  author = {Boldo, Sylvie and Magaud, Nicolas},
  url = {https://hal.inria.fr/hal-01707376},
  booktitle = {{Journ{\'e}es Francophones des Langages Applicatifs 2018}},
  address = {Banyuls-sur-Mer, France},
  editor = {Sylvie Boldo and Nicolas Magaud},
  year = {2018},
  month = jan,
  pdf = {https://hal.inria.fr/hal-01707376/file/jfla2018.pdf},
  hal_id = {hal-01707376},
  hal_version = {v1}
}
@book{BM17,
  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{BJMP17,
  title = {{Formal Verification of a Floating-Point Expansion Renormalization Algorithm}},
  author = {Boldo, Sylvie and Joldes, Mioara and Muller, Jean-Michel and Popescu, Valentina},
  url = {https://hal.archives-ouvertes.fr/hal-01512417},
  booktitle = {{8th International Conference on Interactive Theorem Proving (ITP'2017)}},
  address = {Brasilia, Brazil},
  series = {Lecture Notes in Computer Science},
  volume = {10499},
  year = {2017},
  month = sep,
  pdf = {https://hal.archives-ouvertes.fr/hal-01512417/file/itp17.pdf},
  hal_id = {hal-01512417},
  hal_version = {v1}
}
@inproceedings{BFC17c,
  title = {{Round-off Error Analysis of Explicit One-Step Numerical Integration Methods}},
  author = {Boldo, Sylvie and Faissole, Florian and Chapoutot, Alexandre},
  url = {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}
}
@proceedings{AB17,
  title = {{10th International Workshop on Numerical Software Verification}},
  author = {Abate, Alessandro and Boldo, Sylvie},
  url = {https://hal.inria.fr/hal-01662076},
  booktitle = {{10th International Workshop on Numerical Software Verification}},
  address = {France},
  publisher = {{Springer}},
  year = {2017},
  month = jul,
  hal_id = {hal-01662076},
  hal_version = {v1}
}
@article{BGM17,
  title = {{On the robustness of the 2Sum and Fast2Sum algorithms}},
  author = {Boldo, Sylvie and Graillat, Stef and Muller, Jean-Michel},
  url = {https://hal-ens-lyon.archives-ouvertes.fr/ensl-01310023},
  journal = {{ACM Transactions on Mathematical Software}},
  publisher = {{Association for Computing Machinery}},
  year = {2017},
  volume = {44},
  number = {1},
  month = jul,
  pdf = {https://hal-ens-lyon.archives-ouvertes.fr/ensl-01310023/file/FaithfulTwoSum-Final-Fev2017.pdf}
}
@inproceedings{BCF17b,
  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},
  url = {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}
}
@inproceedings{BCF17a,
  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},
  url = {https://hal.inria.fr/hal-01391578},
  booktitle = {{Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}},
  series = {CPP 2017},
  address = {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}
}
@proceedings{BS17,
  title = {{Vingt-huiti{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs}},
  author = {Boldo, Sylvie and Signoles, Julien},
  url = {https://hal.inria.fr/hal-01662072},
  booktitle = {{Vingt-huiti{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs}},
  address = {Gourette, France},
  year = {2017},
  month = jan,
  hal_id = {hal-01662072},
  hal_version = {v1}
}
@inproceedings{Bol16a,
  title = {{Computing a correct and tight rounding error bound using rounding-to-nearest}},
  author = {Boldo, Sylvie},
  url = {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}
}
@inproceedings{Bol16b,
  title = {{Iterators: where folds fail}},
  author = {Boldo, Sylvie},
  url = {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}
}
@inproceedings{Bol15b,
  title = {{Formal Verification of Programs Computing the Floating-Point Average}},
  author = {Boldo, Sylvie},
  url = {https://hal.inria.fr/hal-01174892},
  booktitle = {{17th International Conference on Formal Engineering Methods}},
  address = {Paris, France},
  publisher = {{Springer International Publishing}},
  year = {2015},
  month = nov,
  pdf = {https://hal.inria.fr/hal-01174892/file/article.pdf},
  editor = {Michael Butler and Sylvain Conchon and Fatiha Za\"idi},
  volume = {9407},
  series = {Lecture Notes in Computer Science},
  pages = {17--32}
}
@inproceedings{Bol15a,
  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,
  url = {http://hal.inria.fr/hal-01148409},
  doi = {http://dx.doi.org/10.1016/j.entcs.2015.10.004},
  volume = {317}
}
@misc{VBMB15,
  title = {{`` Structures : organisation, complexit{\'e}, dynamique '' des mot-cl{\'e}s au sens inattendu}},
  author = {Vi{\'e}ville, Thierry and Boldo, Sylvie and Masseglia, Florent and Bernhard, Pierre},
  url = {https://hal.inria.fr/hal-01238442},
  note = {Article de vulgarisation sur pixees.fr},
  year = {2015},
  month = apr,
  hal_id = {hal-01238442},
  hal_version = {v1}
}
@inbook{Bol14c,
  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/}
}
@article{BJLM15,
  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},
  url = {https://hal.inria.fr/hal-00862689},
  volume = {54},
  number = {2},
  pages = {135-163},
  year = {2015},
  month = feb,
  publisher = {{Springer Verlag (Germany)}}
}
@phdthesis{Bol14a,
  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},
  url = {http://www.lri.fr/~sboldo/files/hdr.pdf}
}
@inproceedings{Bol14b,
  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/}
}
@inbook{BolMul14,
  author = {Sylvie Boldo and Jean-Michel Muller},
  title = {Des ordinateurs capables de calculer plus juste},
  journal = {La Recherche},
  year = {2014},
  number = {492},
  pages = {46--52},
  month = oct
}
@article{BCF14,
  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},
  urlalt = {http://hal.inria.fr/hal-00769201},
  url = {http://www.sciencedirect.com/science/article/pii/S0898122114002636},
  doi = {http://dx.doi.org/10.1016/j.camwa.2014.06.004}
}
@article{BLM15,
  author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
  title = {Coquelicot: A User-Friendly Library of Real Analysis for Coq},
  hal = {http://hal.inria.fr/hal-00860648},
  journal = {Mathematics in Computer Science},
  issn = {1661-8270},
  doi = {10.1007/s11786-014-0181-1},
  year = {2015},
  issn = {1661-8270},
  volume = {9},
  number = {1},
  doi = {10.1007/s11786-014-0181-1},
  url = {http://dx.doi.org/10.1007/s11786-014-0181-1},
  publisher = {Springer Basel},
  pages = {41-62}
}
@article{BLM16,
  author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
  title = {Formalization of Real Analysis: A Survey of Proof Assistants and Libraries},
  url = {http://hal.inria.fr/hal-00806920},
  journal = {Mathematical Structures in Computer Science},
  publisher = {{Cambridge University Press}},
  volume = {26},
  number = {7},
  pages = {1196-1233},
  year = {2016}
}
@inbook{BM13,
  author = {Sylvie Boldo and Guillaume Melquiond},
  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}
}
@inproceedings{Bol13,
  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},
  pages = {91--98},
  month = apr,
  url = {http://hal.inria.fr/hal-00790071}
}
@inproceedings{BJLM13,
  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},
  pages = {107--115},
  month = apr,
  url = {http://hal.inria.fr/hal-00743090}
}
@techreport{Mediation13,
  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 P. 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},
  url = {https://hal.inria.fr/hal-00804915},
  type = {Intern report},
  pages = {34},
  institution = {{none}},
  year = {2013},
  month = mar,
  hal_id = {hal-00804915},
  hal_version = {v1}
}
@inproceedings{BLM12,
  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 The Second International Conference on Certified Programs and Proofs},
  pages = {289--304},
  year = {2012},
  editor = {Chris Hawblitzel and Dale Miller},
  volume = {7679},
  series = {Lecture Notes in Computer Science},
  address = {Kyoto, Japan},
  url = {http://hal.inria.fr/hal-00712938},
  doi = {10.1007/978-3-642-35308-6_22}
}
@article{BCF13,
  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},
  year = {2013},
  month = apr,
  doi = {10.1007/s10817-012-9255-4},
  url = {http://hal.inria.fr/hal-00649240/en/}
}
@inbook{BolVie11a,
  author = {Sylvie Boldo and Thierry Viéville},
  editor = {Gilles Dowek},
  chapter = {Représentation numérique de l’information},
  title = {Introduction à la science informatique},
  pages = {23--72},
  publisher = {CRDP Académie de Paris},
  year = {2011},
  url = {http://crdp.ac-paris.fr/Introduction-a-la-science},
  series = {Repères pour agir},
  month = jul,
  isbn = {2866311884}
}
@inbook{BolVie11b,
  author = {Sylvie Boldo and Thierry Viéville},
  editor = {Gilles Dowek},
  chapter = {Structuration et contrôle de l’information},
  title = {Introduction à la science informatique},
  pages = {281--308},
  publisher = {CRDP Académie de Paris},
  year = {2011},
  url = {http://crdp.ac-paris.fr/Introduction-a-la-science},
  series = {Repères pour agir},
  month = jul,
  isbn = {2866311884}
}
@article{BolMar11,
  author = {Sylvie Boldo and Claude March\'e},
  title = {Formal {V}erification of {N}umerical {P}rograms: from {C}
{A}nnotated {P}rograms to {M}echanical {P}roofs},
  journal = {Mathematics in Computer Science},
  year = {2011},
  publisher = {Birkhauser Basel},
  issn = {1661-8270},
  pages = {377-393},
  volume = {5},
  issue = {4},
  url = {http://dx.doi.org/10.1007/s11786-011-0099-9}
}
@article{BolNgu11,
  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},
  volume = {7},
  issue = {2},
  pages = {151--160},
  month = mar
}
@article{BolMul11,
  author = {Sylvie Boldo and Jean-Michel Muller},
  title = {{E}xact and {A}pproximated error of the {FMA}},
  journal = {IEEE Transactions on Computers},
  publisher = {IEEE Computer Society},
  address = {Los Alamitos, CA, USA},
  year = {2011},
  url = {http://hal.inria.fr/inria-00429617/en/},
  month = feb,
  volume = {60},
  number = {2},
  pages = {157--164}
}
@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},
  year = {2011},
  address = {T{\"u}bingen, Germany},
  month = jul,
  pages = {243--252}
}
@inproceedings{Bol10,
  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},
  note = {NSV-8},
  year = {2010},
  address = {Edinburgh, Scotland},
  month = jul,
  annote = {Invited paper},
  url = {http://hal.inria.fr/inria-00534400/en/}
}
@inproceedings{BCF10,
  author = {Sylvie Boldo and François Clément and Jean-Christophe Filliâtre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
  title = {{Formal Proof of a Wave Equation Resolution Scheme: the Method Error}},
  booktitle = {Proceedings of the first Interactive Theorem Proving Conference (ITP)},
  year = 2010,
  series = {LNCS},
  address = {Edinburgh, Scotland},
  month = jul,
  publisher = {Springer},
  editor = {Matt Kaufmann and Lawrence C. Paulson},
  volume = {6172},
  pages = {147--162},
  note = {(merge of TPHOL and ACL2)},
  url = {http://hal.inria.fr/inria-00450789/en/}
}
@inproceedings{BolNgu10,
  author = {Sylvie Boldo and Thi Minh Tuyen Nguyen},
  title = {Hardware-independent proofs of numerical programs},
  booktitle = {Proceedings of the Second NASA Formal Methods Symposium},
  year = {2010},
  series = {NASA Conference Publication},
  number = {NASA/CP-2010-216215},
  address = {Washington D.C., USA},
  month = apr,
  pages = {14--23},
  editor = {C\'esar Muñoz},
  url = {http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2010-216215.pdf}
}
@misc{Bol10_webtv,
  author = {Sylvie Boldo},
  title = {L'informatique},
  url = {http://www.universcience.tv/media/1340/l-informatique.html},
  month = apr,
  year = 2010,
  howpublished = {Universcience web television},
  note = {Quiz 5-12}
}
@misc{Bol10_I1,
  author = {Sylvie Boldo},
  title = {C'est la faute à l'ordinateur!},
  howpublished = {Interstices -- Id\'ee reçue},
  year = {2010},
  month = feb,
  url = {http://interstices.info/idee-recue-informatique-18}
}
@misc{Bol10_I2,
  author = {Sylvie Boldo},
  title = {Un algorithme de découpe de gâteau},
  howpublished = {Interstices},
  year = {2010},
  month = jul,
  url = {http://interstices.info/decoupe}
}
@inproceedings{BFM09,
  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},
  url = {http://www.lri.fr/~filliatr/publis/calculemus09.pdf}
}
@inproceedings{Bol09b,
  author = {Sylvie Boldo},
  title = {Floats \& {R}opes: a case study for formal numerical program
  verification},
  booktitle = {36th International Colloquium on Automata, Languages and Programming },
  pages = {91--102},
  year = {2009},
  volume = {5556},
  month = jul,
  series = {Lecture Notes in Computer Science - ARCoSS},
  publisher = {Springer},
  address = {Rhodos, Greece},
  doi = {10.1007/978-3-642-02930-1_8},
  url = {http://fost.saclay.inria.fr/files/icalp2009trackb_submission_48.pdf}
}
@article{RZBG09,
  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},
  url = {http://hal.inria.fr/inria-00337537/fr/}
}
@misc{Bol09_I,
  author = {Sylvie Boldo},
  title = {Demandez le programme!},
  howpublished = {Interstices},
  year = {2009},
  month = feb,
  url = {http://interstices.info/demandez-le-programme}
}
@inbook{Bol08DS,
  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,
  url = {http://www.docsciences.fr/-DocSciences-no5-}
}
@misc{Bol08_I2,
  author = {Sylvie Boldo},
  title = {L'informatique, ce n'est pas pour les filles},
  howpublished = {Interstices},
  year = {2008},
  month = sep,
  url = {http://interstices.info/idee-recue-informatique-5}
}
@misc{Bol08_I1,
  author = {Sylvie Boldo},
  title = {Pourquoi mon ordinateur calcule-t-il faux?},
  howpublished = {Interstices},
  year = {2008},
  month = apr,
  note = {Podcast},
  url = {http://interstices.info/a-propos-calcul-ordinateurs}
}
@article{BolDauLi09,
  author = {Sylvie Boldo and Marc Daumas and Ren-Cang Li},
  title = {{F}ormally {V}erified {A}rgument {R}eduction with a {F}used-{M}ultiply-{A}dd},
  journal = {IEEE Transactions on Computers},
  volume = {58},
  number = {8},
  issn = {0018-9340},
  year = {2009},
  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}
}
@article{Bol09a,
  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{BolMel08,
  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},
  doi = {10.1109/TC.2007.70819},
  url = {http://hal.inria.fr/inria-00080427}
}
@inproceedings{BolDauGio08,
  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,
  url = {http://hal.archives-ouvertes.fr/hal-00135090}
}
@inproceedings{BolFil07,
  author = {Sylvie Boldo and Jean-Christophe Filli\^atre},
  title = {Formal Verification of Floating-Point Programs},
  booktitle = {Proceedings of the 18th IEEE Symposium on Computer Arithmetic},
  pages = {187-194},
  year = {2007},
  editor = {Peter Kornerup and Jean-Michel Muller},
  address = {Montpellier, France},
  doi = {10.1109/ARITH.2007.20},
  url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf},
  month = jun
}
@inproceedings{BDKM06,
  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},
  month = sep,
  url = {http://scan2006.uni-due.de/show_abstracts.php?title=+Proof+and+certification+for+an+accurate+discriminant}
}
@inproceedings{Bol06a,
  author = {Sylvie Boldo},
  title = {Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms},
  booktitle = {Proceedings of the third International Joint Conference on Automated Reasoning (IJCAR)},
  year = {2006},
  pages = {52-66},
  address = {Seattle, USA},
  doi = {10.1007/11814771_6},
  month = aug
}
@inproceedings{Bol06b,
  author = {Sylvie Boldo},
  title = {{F}ormal {P}roofs about {DSP}s},
  booktitle = {Algebraic and Numerical Algorithms and Computer-assisted Proofs},
  year = {2006},
  editor = {Bruno Buchberger and Shin'ichi Oishi and Michael Plum and Sigfried M. Rump},
  number = {05391},
  series = {Dagstuhl Seminar Proceedings},
  publisher = {Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany},
  address = {Dagstuhl, Germany},
  url = {http://drops.dagstuhl.de/opus/volltexte/2006/455/pdf/05391_abstracts_collection.455.pdf}
}
@inproceedings{BolMun06,
  author = {Sylvie Boldo and C\'esar Muñ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},
  volume = 2,
  pages = {1328-1332},
  doi = {10.1145/1141277.1141586},
  url = {http://hal.inria.fr/inria-00000892}
}
@inproceedings{BolMul05,
  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},
  doi = {10.1109/ARITH.2005.39},
  editor = {Montuschi, Paolo and Schwarz, Eric},
  pages = {52-58}
}
@inproceedings{BolMel05,
  author = {Sylvie Boldo and Guillaume Melquiond},
  title = {When double rounding is odd},
  year = 2005,
  address = {Paris, France},
  booktitle = {Proceedings of the 17th IMACS World Congress, 
                  Scientific Computation, Applied Mathematics and 
                 Simulation},
  url = {http://hal.archives-ouvertes.fr/inria-00070603/fr/}
}
@phdthesis{Bol04b,
  author = {Sylvie Boldo},
  title = {Preuves formelles en arithm\'etiques \`a virgule flottante},
  school = {\'Ecole Normale Sup\'erieure de Lyon},
  year = {2004},
  month = nov,
  url = {http://www.ens-lyon.fr/LIP/Pub/Rapports/PhD/PhD2004/PhD2004-05.pdf}
}
@article{BolDau04a,
  author = {Boldo, Sylvie and Daumas, Marc},
  title = {Properties of two's complement floating point
                  notations},
  journal = {International Journal on Software Tools for
                  Technology Transfer},
  volume = 5,
  number = {2-3},
  pages = {237-246},
  year = 2004,
  url = {http://hal.archives-ouvertes.fr/hal-00157268},
  doi = {10.1007/s10009-003-0120-y}
}
@article{BolDau04b,
  author = {Sylvie Boldo and Marc Daumas},
  title = {A simple test qualifying the accuracy of Horner's
                  rule for polynomials},
  journal = {Numerical Algorithms},
  year = 2004,
  volume = {37},
  number = {1-4},
  pages = {45-60},
  url = {http://hal.inria.fr/inria-00071879},
  doi = {10.1023/B:NUMA.0000049487.98618.61}
}
@inproceedings{Bol04a,
  author = {Sylvie Boldo},
  booktitle = {Proceedings of the 6th Conference on Real Numbers and 
                   Computers},
  title = {Bridging the gap between formal specification and bit-level
  floating-point arithmetic},
  editor = {Christiane Frougny and Vasco Brattka and Norbert M\"uller},
  year = 2004,
  pages = {22-36},
  address = {Schloss Dagstuhl, Germany},
  url = {http://www.informatik.uni-trier.de/Reports/TR-08-2004/rnc6_04_boldo.pdf}
}
@inproceedings{BolDauThe03,
  author = {Sylvie Boldo and Marc Daumas and Laurent Th{\'e}ry},
  address = {Roma, Italy},
  booktitle = {Proceedings of the 11th Symposium on the Integration
                  of Symbolic Computation and Mechanized Reasoning},
  title = {Formal proofs and computations in finite precision
                  arithmetic},
  year = 2003,
  pages = {101-111},
  url = {http://ftp.lip6.fr/lip6/reports/2003/lip6.2003.010.pdf}
}
@inproceedings{LiBolDau03,
  author = {Ren-Cang Li and Sylvie Boldo and Marc Daumas},
  title = {Theorems on efficient argument reductions},
  pages = {129-136},
  year = 2003,
  address = {Santiago de Compostela, Spain},
  booktitle = {Proceedings of the 16th Symposium on Computer Arithmetic},
  editor = {Bajard, Jean-Claude and Schulte, Michael},
  url = {http://hal.archives-ouvertes.fr/hal-00156244},
  doi = {10.1109/ARITH.2003.1207670}
}
@inproceedings{BolDau03,
  author = {Sylvie Boldo and Marc Daumas},
  title = {Representable correcting terms for possibly
                  underflowing floating point operations},
  pages = {79-86},
  year = 2003,
  address = {Santiago de Compostela, Spain},
  booktitle = {Proceedings of the 16th Symposium on Computer Arithmetic},
  editor = {Bajard, Jean-Claude and Schulte, Michael},
  doi = {10.1109/ARITH.2003.1207663}
}
@inproceedings{BolDau02b,
  author = {Sylvie Boldo and Marc Daumas},
  address = {Paris, France},
  booktitle = {Proceedings of the 10th IMACS-GAMM International 
                  Symposium on Scientific Computing, Computer Arithmetic 
                  and Validated Numerics},
  title = {Faithful rounding without fused multiply and
                  accumulate},
  year = 2002,
  editor = {Lamotte, Jean-Luc and Rico, Fabien},
  pages = {161}
}
@inproceedings{BolDau02a,
  author = {Boldo, Sylvie and Daumas, Marc},
  title = {Properties of the subtraction valid for any floating
                  point system},
  booktitle = {7th International Workshop on Formal Methods for
                  Industrial Critical Systems},
  address = {M{\'a}laga, Spain},
  pages = {137-149},
  year = 2002,
  doi = {doi:10.1016/S1571-0661(04)80408-0},
  url = {http://www.inrialpes.fr/vasy/fmics/workshop-7/proceedings.pdf},
  note = {Also in {\em Electronic Notes in Theoretical Computer Science}, volume~66(2). Elsevier, 2002.}
}
@inproceedings{Bol02,
  author = {Boldo, Sylvie},
  title = {Introduction \`a l'arithm\'etique des ordinateurs},
  booktitle = {Forum des jeunes math\'ematiciennes et des jeunes informaticiennes},
  pages = {7-10},
  year = {2002},
  address = {Paris, France}
}
@inproceedings{BolDau01b,
  author = {Boldo, Sylvie and Daumas, Marc},
  title = {A mechanically validated technique for extending the
                  available precision},
  booktitle = {35th Asilomar Conference on Signals, Systems, and
                  Computers},
  pages = {1299-1303},
  address = {Pacific Grove, California},
  doi = {10.1109/ACSSC.2001.987700},
  year = 2001
}
@inproceedings{BolDau01a,
  author = {Boldo, Sylvie and Daumas, Marc},
  title = {Performances d'implantations de l'addition en
                  pr{\'e}cision quad-double sur diff{\'e}rentes
                  machines},
  pages = {105-112},
  booktitle = {7{\`e}me Symposium sur les Architectures Nouvelles
                  de Machines},
  address = {Paris, France},
  year = 2001,
  url = {http://www.ens-lyon.fr/LIP/Sympa/Sympa7/15.pdf}
}

This file was generated by bibtex2html 1.98.