complete-other.bib

@comment{{This file has been generated by bib2bib 1.97pl3}}
@comment{{Command line: bib2bib -q -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/toccata/web/biblio/bibliodemons/abbrevs.bib /users/demons/filliatr/toccata/web/biblio/bibliodemons/demons.bib /users/demons/filliatr/toccata/web/biblio/bibliodemons/demons2.bib /users/demons/filliatr/toccata/web/biblio/bibliodemons/demons3.bib /users/demons/filliatr/toccata/web/biblio/bibliodemons/team.bib /users/demons/filliatr/toccata/web/biblio/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}
}
@manual{CoqManualV89,
  author = {The {Coq} Development Team},
  title = {The {Coq} Proof Assistant Reference Manual -- Version V8.9},
  year = 2019,
  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}
}
@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{bertails06master,
  author = {Alexandre Bertails},
  title = {Langages synchrones avec horloges p\'eriodiques},
  school = {Master Parisien de Recherche en Informatique},
  month = sep,
  year = 2006,
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport},
  x-pdf = {http://www.lri.fr/~bertails/misc/master_thesis.pdf},
  url = {http://www.lri.fr/~bertails/misc/master_thesis.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{CoqManualV86,
  author = {{The {Coq} Development Team}},
  title = {{The Coq Proof Assistant Reference Manual -- Version V8.6}},
  year = 2016,
  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 = {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},
  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}}
}
@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},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  pdf = {https://gforge.inria.fr/docman/view.php/2990/7919/manual-0.72.pdf},
  rawebnote = {\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},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  pdf = {https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf},
  rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8052/manual-0.73.pdf}}
}
@manual{why3manual080,
  title = {The Why3 platform, version 0.80},
  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.80},
  month = oct,
  year = 2012,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons PROVAL},
  pdf = {https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf},
  note = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}},
  rawebnote = {\url{https://gforge.inria.fr/docman/view.php/2990/8186/manual-0.80.pdf}}
}
@manual{why3manual081,
  title = {The Why3 platform, version 0.81},
  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.81},
  month = mar,
  year = 2013,
  topics = {team},
  keywords = {Why3},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons TOCCATA},
  pdf = {http://why3.lri.fr/download/manual-0.81.pdf},
  note = {\url{http://why3.lri.fr/download/manual-0.81.pdf}},
  hal = {http://hal.inria.fr/hal-00822856/}
}
@manual{why3manual082,
  title = {The Why3 platform, version 0.82},
  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.82},
  month = dec,
  year = 2013,
  topics = {team},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons TOCCATA},
  pdf = {http://why3.lri.fr/download/manual-0.82.pdf},
  note = {\url{http://why3.lri.fr/download/manual-0.82.pdf}},
  hal = {}
}
@manual{why3manual0861,
  title = {The Why3 platform, version 0.86.1},
  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.86.1},
  month = may,
  year = 2015,
  topics = {team},
  x-type = {diffusion},
  x-support = {manuel},
  x-equipes = {demons TOCCATA},
  pdf = {http://why3.lri.fr/download/manual-0.86.1.pdf},
  note = {\url{http://why3.lri.fr/download/manual-0.86.1.pdf}},
  hal = {}
}
@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}
}
@unpublished{lupinski12,
  author = {Nicolas Lupinski and  Joel Falcou and Christine Paulin-Mohring},
  title = {S\'emantiques d'un langage de squelettes},
  topics = {team},
  year = {2012},
  x-equipes = {demons PROVAL archi},
  x-support = {rapport},
  x-type = {article},
  note = {\url{http://www.lri.fr/~paulin/Skel}},
  rawebnote = {\url{http://www.lri.fr/~paulin/Skel}}
}
@unpublished{filliatre13digicosme,
  author = {Jean-Christophe Filli\^atre},
  topics = {team},
  keywords = {Why3},
  title = {Deductive Program Verification with {Why3}},
  year = 2013,
  note = {Lecture notes for the First {DigiCosme} Spring School,
              \url{https://www.lri.fr/~marche/DigiCosmeSchool/filliatre.html}}
}
@mastersthesis{clochard13master,
  topics = {team},
  author = {Martin Clochard},
  title = {Proving Programs with binders, automatically},
  school = {Master Parisien de Recherche en Informatique},
  year = 2013
}
@unpublished{dross13,
  topics = {team},
  hal = {http://hal.inria.fr/hal-00915931},
  title = {Adding Decision Procedures to {SMT} Solvers using Axioms with Triggers},
  author = {Dross, Claire and Conchon, Sylvain and Kanig, Johannes and Paskevich, Andrei},
  abstract = {SMT solvers are efficient tools to decide the
                  satisfiability of ground formulas, including a
                  number of built-in theories such as congruence,
                  linear arithmetic, arrays, and bit-vectors. Adding a
                  theory to that list requires delving into the
                  implementation details of a given SMT solver, and is
                  done mainly by the developers of the solver
                  itself. For many useful theories, one can
                  alternatively provide a first-order
                  axiomatization. However, in the presence of
                  quantifiers, SMT solvers are incomplete and exhibit
                  unpredictable behavior. Consequently, this approach
                  can not provide us with a complete and terminating
                  treatment of the theory of interest. In this paper,
                  we propose a framework to solve this problem, based
                  on the notion of instantiation patterns, also known
                  as triggers. Triggers are annotations that suggest
                  instances which are more likely to be useful in
                  proof search. They are implemented in all SMT
                  solvers that handle first-order logic and are
                  included in the SMT-LIB format. In our framework,
                  the user provides a theory axiomatization with
                  triggers, along with a proof of completeness and
                  termination properties of this axiomatization, and
                  obtains a sound, complete, and terminating solver
                  for her theory in return. We describe and prove a
                  corresponding extension of the traditional Abstract
                  DPLL Modulo Theory framework. Implementing this
                  mechanism in a given SMT solver requires a one-time
                  development effort. We believe that this effort is
                  not greater than that of adding a single decision
                  procedure to the same SMT solver. We have
                  implemented the proposed extension in the Alt-Ergo
                  prover and we discuss some implementation details in
                  the paper. To show that our framework can handle
                  complex theories, we prove completeness and
                  termination of a feature-rich axiomatization of
                  doubly-linked lists. Our tests show that our
                  approach results in a better performance of the
                  solver on goals that stem from the verification of
                  programs manipulating doubly-linked lists.},
  language = {Anglais},
  affiliation = {TOCCATA - INRIA Saclay - {\^I}le-de-France , Laboratoire de Recherche en Informatique - LRI , AdaCore SAS - AdaCore SAS},
  year = 2013,
  pdf = {http://hal.inria.fr/hal-00915931/PDF/dross-article.pdf},
  note = {Submitted}
}
@mastersthesis{ndjanda14,
  topics = {team},
  author = {Mbiada Ndjanda, Jacques Charles},
  title = {{FCLLVM}: un compilateur int\'egr\'e \`a l'environnement {Frama-C}},
  school = {Universit\'e Paris-Diderot},
  year = 2014,
  note = {\url{https://www.lri.fr/~jmbiadan/public/cea_intership_v1.pdf}}
}
@unpublished{conchon:hal-00924646,
  topics = {team},
  title = {A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in {Alt-Ergo}},
  author = {Conchon, Sylvain and Iguernelala, Mohamed and Mebsout, Alain},
  year = 2013,
  hal = {https://hal.archives-ouvertes.fr/hal-00924646}
}
@misc{vieville:hal-01238442,
  topics = {team},
  title = {{ Structures : organisation, complexit\'e, dynamique des mot-cl\'es
                  au sens inattendu}},
  author = {Vieville, Thierry and Boldo, Sylvie and Masseglia, Florent and
                  Bernhard, Pierre},
  year = {2015},
  month = apr,
  hal = {https://hal.inria.fr/hal-01238442},
  note = {Article de vulgarisation sur pixees.fr},
  hal_id = {hal-01238442},
  hal_version = {v1},
  x-scientific-popularization = {yes}
}
@misc{cfpp17,
  topics = {team},
  author = {Arthur Chargu{\'e}raud and Jean-Christophe Filli{\^a}tre and
                  M{\'a}rio Pereira and Fran\c{c}ois Pottier},
  title = {{VOCAL} -- {A} {V}erified {OC}aml {L}ibrary},
  howpublished = {ML Family Workshop},
  month = {September},
  year = {2017},
  hal = {https://hal.inria.fr/hal-01561094}
}
@misc{faissole:hal-01485397,
  topics = {team},
  title = {Synthetic topology in homotopy type theory for probabilistic programming},
  author = {Faissole, Florian and Spitters, Bas},
  howpublished = {PPS 2017 - Workshop on probabilistic programming semantics },
  year = 2017,
  month = jan,
  hal = {https://hal.inria.fr/hal-01485397},
  note = {Poster}
}
@unpublished{clochard18,
  topics = {team},
  title = {Deductive Verification with Ghost Monitors},
  author = {Clochard, Martin and March{\'e}, Claude and Paskevich, Andrei},
  hal = {https://hal.inria.fr/hal-01926659},
  note = {Working paper},
  year = 2018,
  month = nov,
  keywords = {deductive verification ; unstructured programs ; ghost code ; games ; Hoare logic ; predicate transformers ; infinite behaviors}
}
@unpublished{jaloyan18,
  topics = {team},
  title = {Verification of Programs with Pointers in {SPARK}},
  author = {Jaloyan, Georges-Axel and Dross, Claire and Maalej, Maroua and Moy, Yannick and Paskevich, Andrei},
  hal = {https://hal.inria.fr/hal-01936105},
  note = {working paper \url{https://hal.inria.fr/hal-01936105}},
  year = 2018,
  month = nov
}
@unpublished{volkova18a,
  topics = {team},
  title = {Arithmetic approaches for rigorous design of reliable Fixed-Point {LTI} filters},
  author = {Volkova, Anastasia and Hilaire, Thibault and Lauter, Christoph},
  hal = {https://hal.archives-ouvertes.fr/hal-01918650},
  note = {working paper or preprint},
  year = 2018,
  month = nov,
  keywords = {Eigendecomposition ; Gershgorin circles ; Reliable Computations ; Floating-Point Arithmetic ; Digital Filters ; Interval Arithmetic ; Multiple Precision ; Fixed-Point Arithmetic ; Table Maker's Dilemma}
}
@misc{filliatre15mathematicpark,
  author = {Jean-Christophe Filli\^atre},
  title = {V\'erification d\'eductive de programmes},
  howpublished = {Mathematic Park, Institut Henri Poincar\'e},
  url = {https://www.youtube.com/watch?v=Jf5TYvpkXuc},
  year = 2015,
  month = mar,
  note = {S\'eminaire invit\'e},
  topics = {team, lri},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-support = {diffusion},
  x-scientific-popularization = {yes},
  x-invited-conference = {yes}
}
@misc{filliatre18msp,
  author = {Jean-Christophe Filli\^atre},
  title = {An Introduction to Deductive Program Verification},
  howpublished = {Mathematical Summer in Paris (summer school)},
  year = 2018,
  month = jul,
  note = {Cours invit\'e},
  topics = {team, lri},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-support = {diffusion},
  x-international-audience = {yes},
  x-invited-conference = {yes}
}
@misc{filliatre18sem-pour-tous,
  author = {Jean-Christophe Filli\^atre},
  title = {Parcours d'un informaticien},
  howpublished = {S\'eminaire Info Pour Tous},
  url = {https://www.youtube.com/watch?v=LPvZqZV5LKA},
  year = 2018,
  month = sep,
  address = {Paris, France},
  note = {S\'eminaire invit\'e},
  topics = {team, lri},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-support = {diffusion},
  x-invited-conference = {yes}
}
@misc{filliatre17diderot,
  author = {Jean-Christophe Filli\^atre},
  title = {V\'erification d\'eductive de programmes},
  howpublished = {S\'eminaire Acqu\'erir une culture commune
  dans le domaine de l'informatique, lyc\'ee Diderot, Paris},
  year = 2017,
  month = may,
  note = {S\'eminaire invit\'e},
  topics = {team, lri},
  type_publi = {diffusion},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-support = {diffusion},
  x-invited-conference = {yes}
}
@unpublished{becker19wp,
  topics = {team},
  title = {Analysing installation scenarios of {Debian} packages},
  author = {Becker, Benedikt and Jeannerod, Nicolas and March{\'e}, Claude and Regis-Gianas, Yann and Mihaela, Sighireanu and Treinen, Ralf},
  hal = {https://hal.archives-ouvertes.fr/hal-02355602},
  note = {working paper or preprint},
  year = 2019,
  month = nov
}
@unpublished{boldo19wp,
  topics = {team},
  title = {Emulating round-to-nearest-ties-to-zero ''augmented'' floating-point operations using round-to-nearest-ties-to-even arithmetic},
  author = {Boldo, Sylvie and Lauter, Christoph Q. and Muller, Jean-Michel},
  hal = {https://hal.archives-ouvertes.fr/hal-02137968},
  note = {working paper or preprint},
  year = 2019,
  month = oct
}
@unpublished{steinberg19wp,
  topics = {team},
  title = {Quantitative continuity and computable analysis in {Coq}},
  author = {Steinberg, Florian and Thery, Laurent and Thies, Holger},
  hal = {https://hal.inria.fr/hal-02088293},
  note = {working paper or preprint},
  year = 2019,
  month = apr,
  pdf = {https://hal.inria.fr/hal-02088293/file/paper.pdf},
  hal_id = {hal-02088293},
  hal_version = {v1}
}
@misc{steinberg19mla,
  topics = {team},
  title = {Some formal proofs of isomorphy and discontinuity},
  author = {Steinberg, Florian and Thies, Holger},
  hal = {https://hal.inria.fr/hal-02019174},
  howpublished = {Third Workshop on Mathematical Logic and its Applications},
  year = 2019,
  month = mar
}
@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{jfla17,
  topics = {team},
  hal = {https://hal.inria.fr/hal-01662072},
  title = {Journ\'ees Francophones des Langages Applicatifs},
  editor = {Boldo, Sylvie and Signoles, Julien},
  year = 2017,
  booktitle = {Vingt-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  address = {Gourette, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA}
}
@proceedings{jfla18,
  topics = {team},
  title = {Vingt-neuvi\`emes Journ\'ees Francophones des Langages Applicatifs},
  booktitle = {Vingt-neuvi\`emes Journ{\'e}es Francophones des Langages Applicatifs},
  address = {Banyuls-sur-mer, France},
  year = 2018,
  month = jan,
  editor = {Boldo, Sylvie and Magaud, Nicolas},
  hal = {https://hal.inria.fr/hal-01707376}
}
@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}
}
@proceedings{vstte17,
  topics = {team},
  hal = {https://hal.inria.fr/hal-01670145},
  title = {Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference {VSTTE}},
  booktitle = {Verified Software: Theories, Tools, and Experiments. Revised Selected Papers Presented at the 9th International Conference {VSTTE}},
  month = dec,
  year = 2017,
  address = {Heidelberg, Germany},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {VSTTE},
  editor = {Andrei Paskevich and Thomas Wies},
  series = {Lecture Notes in Computer Science},
  number = 10712,
  publisher = {Springer}
}
@proceedings{itp13,
  hal_id = {hal-00908865},
  url = {http://hal.inria.fr/hal-00908865},
  topics = {team},
  title = {{Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings.}},
  editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
  language = {Anglais},
  affiliation = {CELTIQUE - INRIA - IRISA , TOCCATA - INRIA - Laboratoire de Recherche en Informatique - LRI},
  publisher = {Springer},
  pages = {500},
  volume = {7998},
  series = {Lecture Notes in Computer Science},
  audience = {internationale },
  doi = {10.1007/978-3-642-39634-2},
  year = {2013}
}
@proceedings{nsv2017,
  topics = {team},
  title = {10th International Workshop on Numerical Software Verification},
  booktitle = {10th International Workshop on Numerical Software Verification},
  editor = {Abate, Alessandro and Boldo, Sylvie},
  hal = {https://hal.inria.fr/hal-01662076},
  publisher = {{Springer}},
  year = 2017,
  month = jul
}