2014-journal.bib

@comment{{This file has been generated by bib2bib 1.98}}

@comment{{Command line: /usr/bin/bib2bib -q -oc 2014-journal.cite -ob 2014-journal.bib -c 'year = 2014 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{boldo14larecherche,
  hal = {http://hal.inria.fr/ensl-01069744},
  author = {Sylvie Boldo and Jean-Michel Muller},
  title = {Des ordinateurs capables de calculer plus juste},
  journal = {La Recherche},
  year = {2014},
  volume = {492},
  pages = {46--52},
  month = oct,
  topics = {team,lri},
  type_publi = {diffusion}
}

@article{boldo14camwa,
  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},
  hal = {http://hal.inria.fr/hal-00769201},
  url = {http://www.sciencedirect.com/science/article/pii/S0898122114002636},
  doi = {10.1016/j.camwa.2014.06.004},
  topics = {team,lri},
  type_publi = {irevcomlec}
}

@article{marche14scp,
  topics = {team},
  doi = {10.1016/j.scico.2014.04.003},
  hal_id = {hal-00967124},
  hal = {http://hal.inria.fr/hal-00967124/en},
  title = {Verification of the Functional Behavior of a Floating-Point Program: an Industrial Case Study},
  author = {March{\'e}, Claude},
  abstract = {We report on a case study that was conducted as part of an industrial research project on static analysis of critical C code. The example program considered in this paper is an excerpt of an industrial code, only slightly modified for confidentiality reasons, involving floating-point computations. The objective was to establish a property on the functional behavior of this code, taking into account rounding errors made during computations. The property is formalized using ACSL, the behavioral specification language available inside the Frama-C environment, and it is verified by automated theorem proving},
  publisher = {Elsevier},
  journal = {Science of Computer Programming},
  year = 2014,
  volume = 96,
  number = 3,
  pages = {279--296},
  month = mar,
  pdf = {http://hal.inria.fr/hal-00967124/PDF/main.pdf}
}

@article{martindorel14jar,
  topics = {team},
  hal = {http://hal.inria.fr/hal-00919498},
  year = 2014,
  journal = {Journal of Automated Reasoning},
  doi = {10.1007/s10817-014-9312-2},
  title = {Formally Verified Certificate Checkers for Hardest-to-Round Computation},
  publisher = {Springer Netherlands},
  keywords = {Formal proofs; Certificate checkers; Hensel’s lemma; Modular arithmetic},
  author = {Martin-Dorel, {\'E}rik and Hanrot, Guillaume and Mayero, Micaela and Th{\'e}ry, Laurent},
  pages = {1--29},
  language = {English}
}

@article{filliatre14tangente,
  author = {Jean-Christophe Filli\^atre},
  title = {D\'emonstration. L'ordinateur \`a la rescousse},
  journal = {Tangente (hors-s\'erie num\'ero 52)},
  year = 2014,
  number = 52,
  pages = {34--36},
  month = {February},
  topics = {team,lri},
  type_publi = {diffusion}
}