2011-report.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc 2011-report.cite -ob 2011-report.bib -c 'year = 2011 and topics : "team" and ($type="techreport" or $type="manual" or $type="mastersthesis")' /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}}
@manual{moy11jessie,
  title = {The Jessie plugin
for Deduction Verification in Frama-C --- Tutorial and Reference Manual},
  author = {Yannick Moy and Claude March\'e},
  organization = {INRIA \& LRI},
  year = 2011,
  note = {\url{http://krakatoa.lri.fr/}},
  url = {http://krakatoa.lri.fr},
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion},
  x-pdf = {http://krakatoa.lri.fr/jessie.pdf}
}
@techreport{contejean11rr,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest
                  and Olivier Pons and Xavier Urbain},
  title = {{Automated Certified Proofs with CiME3}},
  institution = {C\'edric laboratory, CNAM Paris, France},
  year = {2011},
  number = {2044},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  url = {http://cedric.cnam.fr/fichiers/art_2044.pdf},
  topics = {team},
  abstract = {http://www.lri.fr/~contejea/publis/rr2044/abstract.html}
}
@manual{bobot11why3,
  title = {The Why3 platform},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Guillaume Melquiond and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.64},
  month = feb,
  year = 2011,
  topics = {team},
  keywords = {Why3},
  note = {\url{http://why3.lri.fr/}}
}
@manual{why3manual071,
  title = {The Why3 platform, version 0.71},
  author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and
Claude March\'e and Andrei Paskevich},
  organization = {LRI, CNRS \& Univ. Paris-Sud \& INRIA Saclay},
  edition = {version 0.71},
  month = oct,
  year = 2011,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  note = {\url{https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf}}
}
@techreport{nguyen11rr,
  author = {Thi Minh Tuyen Nguyen and Claude March\'e},
  title = {Proving Floating-Point Numerical Programs by Analysis of
  their Assembly Code},
  institution = {INRIA},
  year = 2011,
  type = {Research Report},
  number = 7655,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/inria-00602266/en/},
  note = {\url{http://hal.inria.fr/inria-00602266/en/}}
}
@techreport{kalyan11rr,
  title = {Automated Generation of Loop Invariants using Predicate Abstraction},
  author = {Kalyanasundaram, Krishnamani and March{\'e}, Claude},
  type = {Research Report},
  institution = {INRIA},
  number = 7714,
  year = 2011,
  month = aug,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  hal = {http://hal.inria.fr/inria-00615623/en/},
  note = {\url{http://hal.inria.fr/inria-00615623/en/}}
}
@techreport{tafat11rr,
  title = {Binary Heaps Formally Verified in {Why3}},
  author = {Tafat, Asma and March{\'e}, Claude},
  type = {Research Report},
  institution = {INRIA},
  number = 7780,
  year = 2011,
  month = oct,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {article},
  topics = {team},
  keywords = {Why3},
  hal = {http://hal.inria.fr/inria-00636083/en/},
  note = {\url{http://hal.inria.fr/inria-00636083/en/}}
}
@techreport{herms11rr,
  title = {A Certified Multi-prover Verification Condition Generator},
  author = {Paolo Herms and Claude March{\'e} and Benjamin Monate},
  x-equipes = {demons PROVAL ext},
  topics = {team},
  institution = {INRIA},
  year = 2011,
  x-support = {rapport},
  x-type = {article},
  hal = {http://hal.inria.fr/hal-00639977/en/},
  note = {\url{http://hal.inria.fr/hal-00639977/en/}},
  type = {Research Report},
  number = 7793
}
@mastersthesis{lelay11master,
  author = {Catherine Lelay},
  title = {\'Etude de la diff\'erentiabilit\'e et de l'int\'egrabilit\'e en {C}oq : Application \`a la formule de d'{A}lembert pour l'\'equation des ondes},
  school = {Universit\'e Paris 7},
  note = {\url{http://www.lri.fr/~lelay/Rapport.pdf}},
  year = 2011,
  topics = {team},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {master}
}
@techreport{BCFMMW11rr,
  hal_id = {hal-00649240},
  hal = {http://hal.inria.fr/hal-00649240/en/},
  title = {Wave Equation Numerical Resolution: Mathematics and Program},
  author = {Boldo, Sylvie and Cl\'ement, Fran\c{c}ois and Filli{\^a}tre, Jean-Christophe and Mayero, Micaela and Melquiond, Guillaume and Weis, Pierre},
  abstract = {We formally prove the C program that implements a simple numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machine-checked.},
  keywords = {Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis},
  language = {Anglais},
  affiliation = {PROVAL - INRIA Saclay - Ile de France , Laboratoire de Recherche en Informatique - LRI , ESTIME - INRIA Rocquencourt , Laboratoire d'informatique de Paris-nord - LIPN , ARENAIRE - Inria Grenoble Rh{\^o}ne-Alpes / LIP Laboratoire de l'Informatique du Parall{\'e}lisme},
  pages = {30},
  type = {Research Report},
  institution = {INRIA},
  number = 7826,
  year = 2011,
  month = dec,
  topics = {team},
  x-equipes = {demons PROVAL ext},
  x-support = {rapport}
}