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