complete-phd.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc complete-phd.cite -ob complete-phd.bib -c 'topics : "team" and $type="phdthesis" and year>=2004' /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}}
@phdthesis{chrzaszcz04phd,
  author = {Jacek Chrz\k{}aszcz},
  title = {Modules in Type Theory with Generative Definitions},
  school = {Warsaw University, Poland and Universit\'e de Paris-Sud},
  year = 2004,
  month = jan,
  type_publi = {these},
  topics = {team}
}
@phdthesis{letouzey2004phd,
  author = {Pierre Letouzey},
  title = {Programmation fonctionnelle certifi{\'e}e: l'extraction de programmes dans l'assistant {Coq}},
  school = {Universit{\'e} Paris-Sud},
  year = 2004,
  month = jul,
  type = {Th{\`e}se de Doctorat},
  topics = {team},
  type_publi = {these},
  url = {http://www.lri.fr/~letouzey/download/these_letouzey.ps.gz}
}
@phdthesis{PhD-Lelay,
  author = {Catherine Lelay},
  title = {Repenser la biblioth\`eque r\'eelle de {Coq} : vers une
                  formalisation de l’analyse classique mieux adapt\'ee},
  type = {Th{\`e}se de Doctorat},
  school = {Universit{\'e} Paris-Sud},
  year = {2015},
  month = jun,
  topics = {team,lri},
  hal = {https://tel.archives-ouvertes.fr/tel-01228517},
  type_publi = {these}
}
@phdthesis{andronick06these,
  author = {June Andronick},
  title = {Mod\'elisation et v\'erification formelles de syst\`emes embarqu\'es dans les cartes \`a microprocessur. Plateforme Java Card et Syst\`eme d'exploitation},
  school = {Universit{\'e} Paris-Sud},
  year = 2006,
  type = {Th{\`e}se de Doctorat},
  month = mar,
  topics = {team},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport}
}
@phdthesis{corbineau05these,
  author = {Pierre Corbineau},
  title = {D\'emonstration Automatique en Th\'eorie des Types},
  school = {Universit{\'e} Paris-Sud},
  year = 2005,
  type = {Th{\`e}se de Doctorat},
  month = sep,
  topics = {team},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport}
}
@phdthesis{Mandel2006phd,
  author = {Louis Mandel},
  title = {Conception, S{\'e}mantique et Implantation de {ReactiveML} : un langage {\`a} la {ML} pour la programmation r{\'e}active},
  school = {Universit{\'e} Paris 6},
  year = {2006},
  x-pdf = {http://www.lri.fr/~mandel/papers/Mandel-These.pdf},
  url = {http://www.lri.fr/~mandel/papers/Mandel-These.pdf},
  topics = {team},
  type_digiteo = {no},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport}
}
@phdthesis{marche05hdr,
  author = {Claude March{\'e}},
  title = {Preuves m{\'e}canis{\'e}es de Propri{\'e}t{\'e}s de Programmes},
  year = {2005},
  month = dec,
  type = {Th\`{e}se d'habilitation},
  school = {Universit{\'e} Paris 11},
  type_publi = {these},
  pdf = {http://www.lri.fr/~marche/marche05hdr.pdf},
  x-equipes = {demons PROVAL},
  x-type = {habilitation},
  x-support = {rapport},
  topics = {team, proval}
}
@phdthesis{oury06these,
  author = {Nicolas Oury},
  title = {{\'E}galit{\'e}s et filtrages avec types d{\'e}pendants dans le Calcul des Constructions Inductives},
  school = {Universit{\'e} Paris-Sud},
  year = 2006,
  month = sep,
  type = {Th{\`e}se de Doctorat},
  topics = {team},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport}
}
@phdthesis{rotaru02phd,
  author = {Mihai Rotaru},
  title = {Sur une th\'eorie unificatrice des mod\`eles de concurrence},
  school = {Cluj University, Romania and Universit\'e de Paris-Sud},
  year = 2004,
  month = jan,
  type_publi = {these},
  topics = {team}
}
@phdthesis{signoles06these,
  author = {Julien Signoles},
  title = {Extension de {ML} avec raffinement : syntaxe, s\'emantiques et syst\`eme de types},
  school = {Universit{\'e} Paris-Sud},
  year = 2006,
  month = jul,
  type = {Th{\`e}se de Doctorat},
  topics = {team},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport}
}
@phdthesis{hubert2008these,
  author = {Thierry Hubert},
  title = {Analyse Statique et preuve de Programmes Industriels Critiques},
  school = {Universit{\'e} Paris-Sud},
  year = 2008,
  type = {Th{\`e}se de Doctorat},
  month = jun,
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport},
  url = {http://www.lri.fr/~marche/hubert08these.pdf}
}
@phdthesis{rousset2008these,
  author = {Nicolas Rousset},
  title = {Automatisation de la Sp\'ecification et de la V\'erification d'applications Java Card},
  school = {Universit{\'e} Paris-Sud},
  year = 2008,
  type = {Th{\`e}se de Doctorat},
  month = jun,
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport},
  url = {http://www.lri.fr/~marche/rousset2008these.pdf}
}
@phdthesis{moy09phd,
  author = {Yannick Moy},
  title = {Automatic Modular Static Safety Checking for C Programs},
  school = {Universit{\'e} Paris-Sud},
  year = 2009,
  month = jan,
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport},
  url = {http://www.lri.fr/~marche/moy09phd.pdf}
}
@phdthesis{sozeau08these,
  author = {Matthieu Sozeau},
  title = {Un environnement pour la programmation avec types d\'ependants},
  school = {Universit{\'e} Paris-Sud},
  year = 2008,
  type = {Th{\`e}se de Doctorat},
  month = dec,
  topics = {team},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport}
}
@phdthesis{plateau10these,
  author = {Florence Plateau},
  title = {Mod{\`e}le n-synchrone pour la programmation de r{\'e}seaux de {Kahn} {\`a} m{\'e}moire born{\'e}e},
  school = {Universit{\'e} Paris-Sud},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {these},
  topics = {team},
  type = {Th{\`e}se de Doctorat},
  year = 2010
}
@phdthesis{urbain10hdr,
  author = {Xavier Urbain},
  title = {Preuve automatique : techniques, outils et certification},
  year = {2010},
  month = nov,
  type = {Th\`{e}se d'habilitation},
  school = {Universit{\'e} Paris-Sud 11},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {habilitation},
  x-support = {rapport},
  topics = {team, proval}
}
@phdthesis{kanig10these,
  author = {Johannes Kanig},
  title = {Sp\'ecification et preuve de programmes d'ordre sup\'erieur},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {these},
  topics = {team},
  year = 2010
}
@phdthesis{lescuyer11these,
  author = {St{\'e}phane Lescuyer},
  title = {Formalisation et d\'eveloppement d'une tactique r\'eflexive pour la
d\'emonstration automatique en {Coq}},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {these},
  url = {http://proval.lri.fr/publications/lescuyer11these.pdf},
  hal = {http://tel.archives-ouvertes.fr/tel-00713668},
  topics = {team},
  year = 2011,
  month = jan
}
@phdthesis{bardou11phd,
  author = {Romain Bardou},
  title = {Verification of Pointer Programs Using Regions and Permissions},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {these},
  url = {http://proval.lri.fr/publications/bardou11phd.pdf},
  note = {\url{http://proval.lri.fr/publications/bardou11phd.pdf}},
  hal = {http://tel.archives-ouvertes.fr/tel-00647331},
  topics = {team},
  year = 2011,
  month = oct
}
@phdthesis{bobot11these,
  author = {Fran\c{c}ois Bobot},
  title = {Logique de s\'eparation et v\'erification d\'eductive},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  x-tel = {http://tel.archives-ouvertes.fr/docs/00/65/25/08/PDF/VD_BOBOT_FRANCOIS_12122011.pdf},
  url = {http://proval.lri.fr/publications/bobot11these.pdf},
  hal = {http://tel.archives-ouvertes.fr/tel-00652508},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {these},
  topics = {team},
  year = 2011,
  month = dec
}
@phdthesis{filliatre11hdr,
  author = {Jean-Christophe Filli\^atre},
  title = {Deductive Program Verification},
  year = 2011,
  month = dec,
  type = {Th\`{e}se d'habilitation},
  school = {Universit{\'e} Paris-Sud},
  type_publi = {these},
  url = {http://www.lri.fr/~filliatr/hdr/memoire.pdf},
  x-equipes = {demons PROVAL},
  x-type = {habilitation},
  x-support = {rapport},
  topics = {team, proval}
}
@phdthesis{nguyen12phd,
  author = {Nguyen, Thi Minh Tuyen},
  title = {Taking architecture and compiler into account
in formal proofs of numerical programs},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  hal = {http://tel.archives-ouvertes.fr/tel-00710193},
  url = {http://proval.lri.fr/publications/tuyennguyen12phd.pdf},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {these},
  topics = {team},
  year = 2012,
  month = jun
}
@phdthesis{conchon12hdr,
  author = {Sylvain Conchon},
  title = {{SMT} Techniques and their Applications: from {Alt-Ergo} to {Cubicle}},
  year = 2012,
  month = dec,
  type = {Th\`{e}se d'habilitation},
  school = {Universit{\'e} Paris-Sud},
  type_publi = {these},
  url = {http://www.lri.fr/~conchon/bib/conchon.html},
  note = {In English, \url{http://www.lri.fr/~conchon/publis/conchonHDR.pdf}},
  rawebnote = {In English, \url{http://www.lri.fr/~conchon/publis/conchonHDR.pdf}},
  x-equipes = {demons PROVAL},
  x-type = {habilitation},
  x-support = {rapport},
  topics = {team}
}
@phdthesis{herms13phd,
  author = {Paolo Herms},
  title = {Certification of a Tool Chain for Deductive Program Verification},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  hal = {http://tel.archives-ouvertes.fr/tel-00789543},
  note = {\url{http://tel.archives-ouvertes.fr/tel-00789543}},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {these},
  topics = {team},
  year = 2013,
  month = jan
}
@phdthesis{iguer13phd,
  author = {Mohamed Iguernelala},
  title = {Strengthening the Heart of an {SMT}-Solver: Design and Implementation of Efficient Decision Procedures},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  hal = {http://tel.archives-ouvertes.fr/tel-00842555},
  x-equipes = {demons ProVal Toccata},
  x-support = {rapport},
  x-type = {these},
  topics = {team},
  year = 2013,
  month = jun
}
@phdthesis{tafat13phd,
  author = {Asma Tafat},
  title = {Preuves par raffinement de programmes avec pointeurs},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  hal = {http://tel.archives-ouvertes.fr/tel-00874679},
  x-equipes = {demons ProVal Toccata},
  x-support = {rapport},
  x-type = {these},
  topics = {team},
  year = 2013,
  month = sep
}
@phdthesis{auger13phd,
  hal = {http://tel.archives-ouvertes.fr/tel-00818169/},
  topics = {team},
  author = {C\'edric Auger},
  title = {Compilation Certifiée de {SCADE/LUSTRE}},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  x-equipes = {demons ProVal Toccata},
  x-support = {rapport},
  x-type = {these},
  note = {\url{http://tel.archives-ouvertes.fr/tel-00818169/}},
  year = 2013,
  month = feb
}
@phdthesis{mebsout14phd,
  title = {Invariants inference for model checking of parameterized systems},
  author = {Mebsout, Alain},
  hal = {https://tel.archives-ouvertes.fr/tel-01073980},
  topics = {team},
  school = {Universit{\'e} Paris-Sud},
  year = 2014,
  month = sep,
  type = {Th{\`e}se de Doctorat}
}
@phdthesis{dross14phd,
  author = {Claire Dross},
  title = {Generic Decision Procedures for Axiomatic First-Order Theories},
  school = {Universit{\'e} Paris-Sud},
  type = {Th{\`e}se de Doctorat},
  hal = {http://tel.archives-ouvertes.fr/tel-01002190},
  x-equipes = {demons ProVal Toccata},
  x-support = {rapport},
  x-type = {these},
  topics = {team},
  year = 2014,
  month = apr
}
@phdthesis{contejean14hdr,
  hal = {https://hal.inria.fr/tel-01089490},
  author = {{\'E}velyne Contejean},
  title = {{Facettes de la preuve, Jeux de reflets entre d{\'e}monstration automatique et preuve assist{\'e}}},
  year = 2014,
  month = jun,
  type = {Th{\`e}se d'habilitation},
  school = {Universit{\'e} Paris-Sud},
  type_publi = {these},
  note = {\url{https://www.lri.fr/~contejea/dossiers/hdr/hdr.pdf}},
  rawebnote = {\url{https://www.lri.fr/~contejea/dossiers/hdr/hdr.pdf}},
  x-equipes = {demons PROVAL},
  x-type = {habilitation},
  x-support = {rapport},
  topics = {team}
}
@phdthesis{boldo14hdr,
  hal = {https://hal.inria.fr/tel-01089643},
  author = {Sylvie Boldo},
  title = {Deductive Formal Verification: How To Make Your Floating-Point Programs Behave},
  year = 2014,
  month = oct,
  type = {Th\`{e}se d'habilitation},
  school = {Universit{\'e} Paris-Sud},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {habilitation},
  x-support = {rapport},
  topics = {team}
}