complete-other.bib

@comment{{This file has been generated by bib2bib 1.97pl2}}
@comment{{Command line: bib2bib -oc complete-other.cite -ob complete-other.bib -c 'topics : "team" and $type<>"book" and $type<>"inbook" and $type<>"incollection" and $type<>"article" and $type<>"inproceedings" and $type<>"phdthesis" and $type<>"techreport" and year>=2004' /users/demons/filliatr/bibliodemons/abbrevs.bib /users/demons/filliatr/bibliodemons/demons.bib /users/demons/filliatr/bibliodemons/demons2.bib /users/demons/filliatr/bibliodemons/demons3.bib /users/demons/filliatr/bibliodemons/team.bib /users/demons/filliatr/bibliodemons/crossrefs.bib}}
@manual{CoqManualV8,
  author = {{The {Coq} Development Team}},
  title = {{The Coq Proof Assistant Reference Manual -- Version V8.0}},
  year = 2004,
  month = apr,
  url = {http://coq.inria.fr},
  note = {\url{http://coq.inria.fr}},
  topics = {team,lri},
  type_publi = {manuel}
}
@manual{CoqTutorialV8,
  author = {G. Huet and G. Kahn and Ch. Paulin-Mohring},
  title = {The {\sf Coq} Proof Assistant - A tutorial - Version 8.0},
  month = apr,
  year = 2004,
  url = {http://coq.inria.fr},
  topics = {team,lri},
  type_publi = {manuel}
}
@mastersthesis{ayache05master,
  author = {Nicolas Ayache},
  title = {Coop\'eration d'outils de preuve interactifs et automatiques},
  school = {Universit{\'e} Paris 7},
  year = 2005,
  topics = {team},
  type_publi = {rapport},
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport}
}
@mastersthesis{iguernelala09master,
  author = {Mohamed Iguernelala},
  title = {{Extension modulo Associativit\'e-Commutativit\'e
  de l'algorithme de cl\^oture par congruence CC(X)}},
  school = {Universit{\'e} Paris-Sud},
  year = 2009,
  topics = {team},
  type_publi = {rapport},
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport}
}
@mastersthesis{bardou07master,
  author = {Romain Bardou},
  title = {Invariants de classe et syst\`emes d'ownership},
  school = {Master Parisien de Recherche en Informatique},
  topics = {team},
  type_publi = {rapport},
  type_digiteo = {no},
  year = 2007,
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport},
  x-pdf = {http://romain.bardou.fr/papers/stage2007r.pdf},
  url = {http://romain.bardou.fr/papers/stage2007r.pdf}
}
@mastersthesis{kanig07master,
  author = {Johannes Kanig},
  title = {Certifying a Congruence Closure algorithm in {Coq} using Traces},
  school = {Technische Universit\"at Dresden},
  year = 2007,
  topics = {team, lri},
  month = apr,
  type = {Diplomarbeit}
}
@mastersthesis{beauquier08master,
  author = {Maxime Beauquier},
  title = {Application du filtrage modulo associativit\'e et commutativit\'e ({AC}) \`a la r\'e\'ecriture de sous-termes modulo {AC} dans {Coq}},
  school = {Master Parisien de Recherche en Informatique},
  topics = {team},
  type_publi = {rapport},
  type_digiteo = {no},
  year = 2008,
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport}
}
@mastersthesis{bobot08master,
  author = {Fran\c{c}ois Bobot},
  title = {Satisfiabilit\'e de formules closes modulo une th\'eorie avec \'egalit\'e
et pr\'edicats},
  school = {Master Parisien de Recherche en Informatique},
  topics = {team},
  type_publi = {rapport},
  type_digiteo = {no},
  year = 2008,
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport}
}
@mastersthesis{gay08master,
  author = {Steven Gay},
  title = {Analyse d'\'echappement de port\'ee en {ReactiveML}},
  school = {Master Parisien de Recherche en Informatique},
  topics = {team},
  type_publi = {rapport},
  type_digiteo = {no},
  year = 2008,
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport}
}
@misc{cime3,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
  title = {{CiME3}},
  year = 2007,
  url = {{http://cime.lri.fr}},
  note = {\url{http://cime.lri.fr}},
  topics = {team,lri},
  type_publi = {autre},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@misc{coccinelle,
  author = {\'Evelyne Contejean},
  title = {{Coccinelle}},
  year = 2005,
  url = {{http://www.lri.fr/~contejea/Coccinelle/coccinelle.html}},
  note = {\url{http://www.lri.fr/~contejea/Coccinelle/coccinelle.html}},
  topics = {team,lri},
  type_publi = {autre},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@misc{alt-ergo,
  author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala and St\'ephane Lescuyer and Alain Mebsout},
  title = {The {Alt-Ergo} Automated Theorem Prover},
  note = {\url{http://alt-ergo.lri.fr/}},
  topics = {team,lri},
  year = 2008,
  x-equipes = {demons PROVAL}
}
@misc{ergo,
  author = {Sylvain Conchon and \'Evelyne Contejean},
  title = {The {Alt-Ergo} automatic Theorem Prover},
  url = {http://alt-ergo.lri.fr/},
  howpublished = {\url{http://alt-ergo.lri.fr/}},
  note = {APP deposit under the number IDDN FR 001 110026 000 S P 2010 000 1000},
  topics = {team,lri},
  year = 2008,
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@misc{filliatr07queens,
  author = {Jean-Christophe Filli\^atre},
  title = {{Queens on a Chessboard:
       an Exercise in Program Verification}},
  topics = {team, lri},
  type_publi = {autre},
  type_digiteo = {no},
  x-equipes = {demons PROVAL EXT},
  x-type = {manuel},
  x-support = {diffusion},
  year = 2007,
  note = {\url{http://why.lri.fr/queens/}},
  url = {http://why.lri.fr/queens/},
  x-pdf = {http://why.lri.fr/queens/queens.ps}
}
@mastersthesis{hubert04dea,
  author = {Thierry Hubert},
  title = {{Certification des preuves de terminaison en Coq}},
  type = {Rapport de {DEA}},
  year = 2004,
  month = sep,
  school = {Universit{\'e} Paris 7},
  topics = {team, lri},
  note = {\url{http://www.lri.fr/~marche/hubert04rr.ps}},
  url = {http://www.lri.fr/~marche/hubert04rr.ps}
}
@manual{MandelMaranget2007Jocaml,
  author = {Louis Mandel and Luc Maranget},
  title = {The {JoCaml} system},
  institution = {Inria-Rocquencourt},
  note = {Software and documentation available at
                    \url{http://jocaml.inria.fr/}},
  year = 2007,
  url = {http://jocaml.inria.fr/},
  x-equipes = {demons PROVAL EXT},
  x-type = {manuel},
  x-support = {diffusion},
  topics = {team}
}
@mastersthesis{sozeau05master,
  author = {Matthieu Sozeau},
  title = {{Coercion par pr{\'e}dicats en {Coq}}},
  school = {Universit{\'e} Paris 7},
  year = 2005,
  note = {In French},
  topics = {team},
  type_publi = {rapport},
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport},
  url = {http://mattam.org/research/publications/Coercion par prédicats en Coq.pdf}
}
@manual{baudin08acsl,
  title = {ACSL: ANSI/ISO C Specification Language},
  author = {Patrick Baudin  and Jean-Christophe Filli\^atre and Claude March\'e and Benjamin Monate and Yannick Moy and Virgile Prevosto},
  year = 2008,
  note = {\url{http://frama-c.cea.fr/acsl.html}},
  url = {http://frama-c.cea.fr/acsl.html},
  x-pdf = {http://frama-c.cea.fr/download/acsl_1.4.pdf},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {contrat},
  x-support = {rapport}
}
@manual{baudin09acsl,
  title = {ACSL: ANSI/ISO C Specification Language, version 1.4},
  author = {Patrick Baudin  and Jean-Christophe Filli\^atre and Claude March\'e and Benjamin Monate and Yannick Moy and Virgile Prevosto},
  year = 2009,
  note = {\url{http://frama-c.cea.fr/acsl.html}},
  url = {http://frama-c.cea.fr/acsl.html},
  x-pdf = {http://frama-c.cea.fr/download/acsl_1.4.pdf},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {contrat},
  x-support = {rapport}
}
@manual{lucy:manual06,
  author = {Marc Pouzet},
  title = {{Lucid Synchrone}, version 3.
                   Tutorial and reference manual},
  organization = {Universit\'e Paris-Sud, LRI},
  month = apr,
  year = 2006,
  topics = {team},
  type_publi = {autre},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion},
  url = {http://www.lri.fr/~pouzet/lucid-synchrone}
}
@mastersthesis{lescuyer06master,
  author = {St\'ephane Lescuyer},
  title = {Codage de la logique du premier ordre polymorphe multi-sort\'ee
dans la logique sans sortes},
  school = {Master Parisien de Recherche en Informatique},
  topics = {team},
  type_publi = {rapport},
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport},
  year = 2006
}
@manual{CoqManualV82,
  author = {{The {Coq} Development Team}},
  title = {{The Coq Proof Assistant Reference Manual -- Version V8.2}},
  year = 2008,
  note = {\url{http://coq.inria.fr}},
  url = {http://coq.inria.fr},
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL EXT},
  x-type = {manuel},
  x-support = {diffusion}
}
@manual{CoqManualV83,
  author = {{The {Coq} Development Team}},
  title = {{The Coq Proof Assistant Reference Manual -- Version V8.3}},
  year = 2010,
  note = {\url{http://coq.inria.fr}},
  url = {http://coq.inria.fr},
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL EXT},
  x-type = {manuel},
  x-support = {diffusion}
}
@manual{CoqSetoidV82,
  author = {Matthieu Sozeau},
  note = {Chapter of {The Coq Proof Assistant Reference Manual -- Version V8.2}},
  title = {User defined equalities and relations},
  institution = {INRIA},
  year = 2008,
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@manual{CoqProgramV82,
  author = {Matthieu Sozeau},
  note = {Chapter of {The Coq Proof Assistant Reference Manual -- Version V8.2}, \url{http://coq.inria.fr/}},
  title = {Program},
  url = {http://coq.inria.fr/},
  year = 2008,
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@manual{CoqTypeClassesV82,
  author = {Matthieu Sozeau},
  title = {Type Classes},
  note = {Chapter of {The Coq Proof Assistant Reference Manual -- Version V8.2}},
  organization = {INRIA},
  year = 2008,
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@manual{CoqManualV81,
  author = {{The {Coq} Development Team}},
  title = {{The Coq Proof Assistant Reference Manual -- Version V8.1}},
  year = 2006,
  month = jul,
  url = {http://coq.inria.fr},
  note = {\url{http://coq.inria.fr}},
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL EXT},
  x-type = {manuel},
  x-support = {diffusion}
}
@misc{boldo09diffusion,
  author = {Sylvie Boldo},
  title = {Demandez le programme!},
  howpublished = {Interstices},
  year = {2009},
  month = feb,
  topics = {team, lri},
  url = {http://interstices.info/demandez-le-programme},
  note = {\url{http://interstices.info/demandez-le-programme}},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {diffusion},
  x-scientific-popularization = {yes}
}
@manual{moy08manual,
  title = {Jessie Plugin Tutorial, \emph{Lithium} version},
  author = {Yannick Moy and Claude March\'e},
  organization = {INRIA},
  year = 2008,
  note = {\url{http://www.frama-c.cea.fr/jessie.html}},
  url = {http://www.frama-c.cea.fr/jessie.html},
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion},
  x-pdf = {http://www.frama-c.cea.fr/jessie/main.pdf}
}
@manual{moy09manual,
  title = {Jessie Plugin Tutorial, \emph{Beryllium} version},
  author = {Yannick Moy and Claude March\'e},
  organization = {INRIA},
  year = 2009,
  note = {\url{http://www.frama-c.cea.fr/jessie.html}},
  url = {http://www.frama-c.cea.fr/jessie.html},
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion},
  x-pdf = {http://www.frama-c.cea.fr/jessie/main.pdf}
}
@manual{moy10manual,
  title = {Jessie Plugin, \emph{Boron} version},
  author = {Yannick Moy and Claude March\'e},
  organization = {INRIA},
  year = 2010,
  note = {\url{http://frama-c.com/jessie/jessie-tutorial.pdf}},
  url = {http://frama-c.com/jessie/jessie-tutorial.pdf},
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion},
  x-pdf = {http://frama-c.com/jessie/jessie-tutorial.pdf}
}
@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}
}
@misc{ayad09,
  author = {Ali Ayad and Claude March\'e},
  title = {Behavioral Properties of Floating-Point Programs},
  howpublished = {Hisseo publications},
  year = 2009,
  note = {\url{http://hisseo.saclay.inria.fr/ayad09.pdf}},
  url = {http://hisseo.saclay.inria.fr/ayad09.pdf},
  topics = {team}
}
@mastersthesis{tafat09master,
  author = {Asma Tafat},
  title = {Invariants et raffinements en
pr\'esence de partage},
  school = {Universit\'e Paris 6},
  topics = {team},
  year = 2009,
  url = {http://www.lri.fr/~marche/tafat09master.pdf}
}
@unpublished{milchior09,
  author = {Arthur Milchior},
  title = {Algorithme de matching, modulo \'egalit\'e, incr\'emental, typ\'e et persistant},
  institution = {\'Ecole Normale Sup\'erieure, Paris},
  note = {Rapport de stage L3},
  rawebnote = {Rapport de stage L3},
  topics = {team},
  year = 2009
}
@misc{marche09ws,
  author = {Claude March\'e},
  title = {The {Krakatoa} tool for Deductive Verification of {Java}
                  Programs},
  howpublished = {Winter School on Object-Oriented Verification,
                  Viinistu, Estonia},
  month = jan,
  year = 2009,
  url = {http://krakatoa.lri.fr/ws/},
  x-pdf = {http://krakatoa.lri.fr/ws/notes.pdf},
  note = {\url{http://krakatoa.lri.fr/ws/}},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-support = {diffusion},
  x-type = {invitation}
}
@misc{boldo10diffusion,
  author = {Sylvie Boldo},
  title = {C'est la faute \`a l'ordinateur!},
  howpublished = {Interstices -- Id\'ee re\c{c}ue},
  year = {2010},
  month = feb,
  topics = {team, lri},
  note = {\url{http://interstices.info/idee-recue-informatique-18}},
  web = {http://interstices.info/idee-recue-informatique-18},
  hal = {http://hal.inria.fr/inria-00534848/fr/},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {diffusion},
  x-scientific-popularization = {yes}
}
@misc{boldo10-webtv,
  author = {Sylvie Boldo},
  x-equipes = {demons PROVAL},
  x-support = {video},
  x-type = {vulgarisation},
  topics = {team},
  title = {L'informatique},
  web = {http://www.universcience.tv/media/1340/l-informatique.html},
  note = {Quiz 5-12, \url{http://www.universcience.tv/media/1340/l-informatique.html}},
  hal = {http://hal.inria.fr/inria-00534852/fr/},
  month = apr,
  year = 2010,
  howpublished = {Universcience web television},
  x-scientific-popularization = {yes}
}
@mastersthesis{herms09master,
  author = {Paolo Herms},
  title = {Partial Type Inference with Higher-Order Types},
  school = {Universit\`a di Pisa},
  year = 2009,
  topics = {team}
}
@proceedings{audebaud10scp,
  title = {Science of Computer Programming. Special issue on the Mathematics of Program Construction (MPC 2008)},
  year = 2011,
  volume = 76,
  number = 3,
  issn = {0167-6423},
  doi = {DOI: 10.1016/j.scico.2010.05.005},
  x-equipes = {demons PROVAL ext},
  x-support = {livre},
  x-type = {editorial},
  topics = {team},
  publisher = {Elsevier Science Publishers},
  x-proceedings = {yes},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  url = {http://www.sciencedirect.com/science/article/B6V17-508CCPM-1/2/05b9e659a964af2a63a054fe26f63705},
  editor = {Philippe Audebaud and Christine Paulin-Mohring}
}
@misc{boldo08diffusion-2,
  author = {Sylvie Boldo and Thierry Vi\'eville},
  title = {L'informatique, ce n'est pas pour les filles},
  howpublished = {Interstices},
  year = {2008},
  topics = {team},
  month = sep,
  url = {http://interstices.info/idee-recue-informatique-5},
  note = {\url{http://interstices.info/idee-recue-informatique-5}},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {diffusion},
  x-scientific-popularization = {yes}
}
@misc{boldo10diffusion-2,
  author = {Sylvie Boldo},
  title = {Un algorithme de d\'ecoupe de g\^ateau},
  howpublished = {Interstices},
  year = {2010},
  topics = {team},
  month = jul,
  url = {http://interstices.info/decoupe},
  note = {\url{http://interstices.info/decoupe}},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {diffusion},
  x-scientific-popularization = {yes}
}
@misc{boldopodcast08,
  author = {Sylvie Boldo},
  title = {Pourquoi mon ordinateur calcule-t-il faux?},
  howpublished = {Interstices},
  year = {2008},
  month = apr,
  topics = {team},
  note = {Podcast, \url{http://interstices.info/a-propos-calcul-ordinateurs}},
  url = {http://interstices.info/a-propos-calcul-ordinateurs},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {diffusion},
  x-scientific-popularization = {yes}
}
@misc{BobotPaskevich2011,
  author = {Fran\c{c}ois Bobot and Andrei Paskevich},
  title = {{Expressing Polymorphic Types in a Many-Sorted Language}},
  year = 2011,
  topics = {team},
  note = {Preliminary report. \url{http://hal.inria.fr/inria-00591414/}}
}
@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},
  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},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  note = {\url{https://gforge.inria.fr/docman/view.php/2990/7635/manual.pdf}}
}
@manual{why3manual072,
  title = {The Why3 platform, version 0.72},
  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.72},
  month = may,
  year = 2012,
  topics = {team},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  note = {\url{https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf}}
}
@manual{why3manual073,
  title = {The Why3 platform, version 0.73},
  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.73},
  month = jul,
  year = 2012,
  topics = {team},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  note = {\url{https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf}}
}
@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}
}
@misc{gasparcoq2011,
  author = {Nuno Gaspar},
  title = {Mechanized Semantics into Concurrent Program verification},
  howpublished = {\url{http://www.lri.fr/~gaspar/rgcoq.html}},
  topics = {team},
  month = sep,
  year = 2011,
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {master},
  note = {A documented Coq library, work in progress}
}
@proceedings{types04,
  editor = {Jean-Christophe Filli\^atre and Christine Paulin-Mohring and Benjamin Werner},
  title = {Types for Proofs and Programs, International Workshop, TYPES
               2004, Jouy-en-Josas, France, December 15-18,2004, Selected Papers},
  booktitle = {TYPES 2004},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3839},
  year = {2005},
  topics = {team,lri},
  isbn = {3-540-31428-8},
  x-equipes = {demons PROVAL EXT},
  x-type = {edition},
  x-support = {actes}
}
@proceedings{mpc08,
  editor = {Philippe Audebaud and Christine Paulin-Mohring},
  title = {Mathematics of Program Construction, MPC 2008},
  booktitle = {Mathematics of Program Construction, MPC 2008},
  publisher = {Springer},
  address = {Marseille, France},
  month = jul,
  series = {Lecture Notes in Computer Science},
  volume = {5133},
  topics = {team,lri},
  year = {2008},
  x-equipes = {demons PROVAL EXT},
  x-type = {edition},
  url = {http://www.springerlink.com/content/978-3-540-70593-2},
  x-support = {actes}
}
@proceedings{postfoveoos10,
  editor = {Bernhard Beckert and Claude March\'e},
  title = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010},
  booktitle = {Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010},
  publisher = {Springer},
  topics = {team},
  series = {Lecture Notes in Computer Science},
  volume = 6528,
  month = jan,
  year = 2011,
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-equipes = {demons PROVAL ext},
  x-support = {actes},
  x-type = {edition},
  x-cle-support = {FOVEOOS},
  x-pays = {DE}
}