boldo_ref.bib
@incollection{BolVie11a,
author = {Sylvie Boldo and Thierry Viéville},
editor = {Gilles Dowek},
title = {Représentation numérique de l’information},
booktitle = {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}
}
@incollection{BolVie11b,
author = {Sylvie Boldo and Thierry Viéville},
editor = {Gilles Dowek},
title = {Structuration et contrôle de l’information},
booktitle = {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},
pages = {1--10},
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übingen, Germany},
month = jul
}
@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 = july,
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}
}
@incollection{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.96.
