2011-journal.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc 2011-journal.cite -ob 2011-journal.bib -c 'year = 2011 and topics : "team" and $type="article"' /home/marche/biblio/abbrevs.bib /home/marche/biblio/demons.bib /home/marche/biblio/demons2.bib /home/marche/biblio/demons3.bib /home/marche/biblio/team.bib /home/marche/biblio/crossrefs.bib}}
@article{boldo10-tc,
  title = {Exact and {A}pproximated error of the {FMA}},
  author = {Boldo, Sylvie and Muller, Jean-Michel},
  abstract = {The fused multiply accumulate-add (FMA) instruction,
                  specified by the IEEE 754-2008 Standard for
                  Floating-Point Arithmetic, eases some calculations,
                  and is already available on some current processors
                  such as the Power PC or the Itanium. We first extend
                  an earlier work on the computation of the exact
                  error of an FMA (by giving more general conditions
                  and providing a formal proof). Then, we present a
                  new algorithm that computes an approximation to the
                  error of an FMA, and provide error bounds and a
                  formal proof for that algorithm.},
  journal = {IEEE Transactions on Computers},
  publisher = {IEEE Computer Society},
  address = {Los Alamitos, CA, USA},
  year = {2011},
  month = feb,
  volume = {60},
  number = {2},
  pages = {157--164},
  hal = {http://hal.inria.fr/inria-00429617/en/},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-support = {diffusion},
  x-type = {article}
}
@article{dinechin10tc,
  hal = {http://hal.inria.fr/inria-00533968/en/},
  title = {Certifying the floating-point implementation of an elementary function using {G}appa},
  author = {de Dinechin, Florent and Lauter, Christoph and Melquiond, Guillaume},
  publisher = {{IEEE} Comp. Soc. Press},
  journal = {{IEEE} {T}ransactions on {C}omputers },
  pages = {242--253},
  volume = {60},
  number = {2},
  x-equipes = {demons PROVAL ext},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-pays = {US},
  topics = {team},
  doi = {10.1109/TC.2010.128},
  year = 2011
}
@article{boldo11-isse,
  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},
  pages = {151--160},
  volume = {7},
  issue = {2},
  hal = {http://hal.inria.fr/hal-00777639},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  topics = {team},
  x-support = {revue},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-cle-support = {ISSE}
}
@article{boldo11mcs,
  author = {Sylvie Boldo and Claude March\'e},
  title = {Formal verification of numerical programs: from {C} annotated programs to mechanical proofs},
  journal = {Mathematics in Computer Science},
  topics = {team},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {MCS},
  x-equipes = {demons PROVAL},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  year = 2011,
  publisher = {Birkhauser Basel},
  issn = {1661-8270},
  pages = {377--393},
  volume = {5},
  issue = {4},
  doi = {10.1007/s11786-011-0099-9},
  url = {http://proval.lri.fr/publications/boldo11mcs.pdf},
  hal = {http://hal.inria.fr/hal-00777605}
}
@article{filliatre11sttt,
  author = {Jean-Christophe Filli\^atre},
  title = {Deductive Software Verification},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  month = aug,
  year = 2011,
  publisher = {Springer Berlin / Heidelberg},
  volume = 13,
  number = 5,
  pages = {397-403},
  issn = {1433-2779},
  x-type = {article},
  x-support = {revue},
  x-equipes = {demons PROVAL},
  x-cle-support = {STTT},
  doi = {10.1007/s10009-011-0211-0},
  url = {http://proval.lri.fr/publications/filliatre11sttt.pdf},
  abstract = {Deductive software verification, also known as program proving,
  expresses the correctness of a program as a set
  of mathematical statements, called verification conditions. They are
  then discharged using either automated or interactive theorem
  provers. We briefly review this research area, with an emphasis on
  tools.},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-international-audience = {yes},
  x-editorial-board = {yes}
}