Publications of Sylvie Boldo

boldo_ref.bib

@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},
  note = {To be published},
  journal = {{ACM Transactions on Mathematical Software}},
  publisher = {{Association for Computing Machinery}},
  year = {2017}
}
@inproceedings{BCF17,
  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 = {{6th ACM SIGPLAN Conference on Certified Programs and Proofs}},
  address = {Paris, France},
  year = {2017},
  month = jan,
  pdf = {https://hal.inria.fr/hal-01391578/file/article.pdf}
}
@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}
}
@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}
}
@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.