2011-report.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2011-report.cite -ob 2011-report.bib -c 'year = 2011 and topics : "team" and ($type="techreport" or $type="manual" or $type="mastersthesis")' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../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.org/}}
}
@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}
}