2015-journal.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2015-journal.cite -ob 2015-journal.bib -c 'year = 2015 and topics : "team" and $type="article"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@article{boldo14jar,
author = {Boldo, Sylvie and Jourdan, Jacques-Henri and Leroy, Xavier and Melquiond, Guillaume},
title = {{Verified Compilation of Floating-Point Computations}},
journal = {Journal of Automated Reasoning},
volume = {54},
number = {2},
pages = {135-163},
year = {2015},
month = feb,
publisher = {{Springer Verlag (Germany)}},
hal = {https://hal.inria.fr/hal-00862689},
topics = {team,lri},
type_publi = {irevcomlec}
}
@article{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{bobot14sttt,
topics = {team},
doi = {10.1007/s10009-014-0314-5},
hal_id = {hal-00967132},
hal = {http://hal.inria.fr/hal-00967132/en},
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {Let's Verify This with {Why3}},
journal = {International Journal on Software Tools for Technology Transfer (STTT)},
volume = 17,
number = 6,
pages = {709--727},
year = 2015,
note = {See also \url{http://toccata.gitlabpages.inria.fr/toccata/gallery/fm2012comp.en.html}},
publisher = {Springer Berlin / Heidelberg},
x-type = {article},
x-support = {revue},
x-cle-support = {STTT},
x-international-audience = {yes},
x-editorial-board = {yes}
}
@article{marche15ercim,
topics = {team},
hal = {http://hal.inria.fr/hal-01102242},
author = {Claude March\'e and Johannes Kanig},
title = {Bridging the Gap between Testing and Formal
Verification in {Ada} Development},
journal = {ERCIM News},
year = 2015,
volume = 100,
pages = {38--39},
month = jan
}
@article{roux15jar,
topics = {team},
title = {Formal Proofs of Rounding Error Bounds},
author = {Roux, Pierre},
hal = {https://hal.archives-ouvertes.fr/hal-01091189},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
year = 2015,
doi = {10.1007/s10817-015-9339-z},
keywords = {floating-point arithmetic ; rounding error ; numerical analysis ; proof assistant ; Coq ; matrices ; Cholesky decomposition}
}
@article{martindorel15jarb,
topics = {team},
title = {Formally verified certificate checkers for hardest-to-round computation},
author = {Martin-Dorel, {\'E}rik and Hanrot, Guillaume and Mayero, Micaela and Th{\'e}ry, Laurent},
hal = {https://hal.inria.fr/hal-00919498},
journal = {Journal of Automated Reasoning},
publisher = {Springer},
volume = 54,
number = 1,
pages = {1-29},
year = 2015,
doi = {10.1007/s10817-014-9312-2},
keywords = {formal proofs ; certificate checkers ; Hensel's lemma ; modular arithmetic}
}