complete-phd.bib

@comment{{This file has been generated by bib2bib 1.98}}

@comment{{Command line: /usr/bin/bib2bib -q -oc complete-phd.cite -ob complete-phd.bib -c 'topics : "team" and $type="phdthesis" and year>=2004' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../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 = {https://usr.lmf.cnrs.fr/~jcf/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{gondelman16phd,
  topics = {team},
  title = {A Pragmatic Type System for Deductive Software Verification},
  author = {Gondelman, L{\'e}on},
  hal = {https://tel.archives-ouvertes.fr/tel-01619603},
  school = {Universit{\'e} Paris-Saclay},
  year = 2016,
  type = {Th{\`e}se de Doctorat}
}

@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}
}

@phdthesis{clochard18phd,
  topics = {team},
  title = {M\'ethodes et outils pour la sp\'ecification et la preuve de propri\'et\'es difficiles de programmes s\'equentiels},
  author = {Clochard, Martin},
  hal = {https://tel.archives-ouvertes.fr/tel-01787689},
  number = {2018SACLS071},
  school = {Universit{\'e} Paris-Saclay},
  year = 2018,
  month = mar,
  type = {Th{\`e}se de Doctorat}
}

@phdthesis{declerck18phd,
  topics = {team},
  title = {Verification via {Model Checking} of Parameterized Concurrent Programs on Weak Memory Models},
  author = {Declerck, David},
  hal = {https://tel.archives-ouvertes.fr/tel-01900842},
  school = {Universit{\'e} Paris-Saclay},
  year = 2018,
  month = sep,
  keywords = {Weak memory ; Model checking ; Verification ; M{\'e}moire faible},
  type = {Th{\`e}se de Doctorat}
}

@phdthesis{pereira18phd,
  topics = {team},
  title = {Tools and Techniques for the Verification of Modular Stateful Code},
  author = {Pereira, M{\'a}rio},
  school = {Universit{\'e} Paris-Saclay},
  year = 2018,
  month = dec,
  type = {Th{\`e}se de Doctorat}
}

@phdthesis{melquiond19hdr,
  topics = {team},
  title = {Formal Verification for Numerical Computations, and the Other Way Around},
  author = {Melquiond, Guillaume},
  hal = {https://tel.archives-ouvertes.fr/tel-02194683},
  school = {Universit\'e Paris Sud},
  year = 2019,
  month = apr,
  type = {Habilitation \`a diriger des recherches}
}

@phdthesis{rieuhelft20phd,
  topics = {team},
  title = {Development and verification of arbitrary-precision integer arithmetic libraries},
  author = {Rieu-Helft, Rapha{\"e}l},
  hal = {https://tel.archives-ouvertes.fr/tel-03032942},
  school = {Universit{\'e} Paris-Saclay},
  year = 2020,
  keywords = {Static analysis ; Arbitrary-precision integer arithmetic ; Deductive verification of programs ; Proof by reflection ; Why3 ; V{\'e}rification d{\'e}ductive de programmes ; Arithm{\'e}tique enti{\`e}re en pr{\'e}cision arbitraire ; Analyse statique ; Preuve par r{\'e}flexion ; Why3},
  type = {Th{\`e}se de Doctorat}
}

@phdthesis{garchery22phd,
  topics = {team},
  title = {Certification de la transformation de t{\^a}ches de preuve},
  author = {Garchery, Quentin},
  hal = {https://theses.hal.science/tel-03560564},
  number = {2022UPASG006},
  school = {Universit{\'e} Paris-Saclay},
  year = 2022,
  type = {Th{\`e}se de Doctorat}
}

@phdthesis{coquereau19phd,
  topics = {team},
  title = {Am{\'e}lioration de performances du solveur {SMT} {Alt-Ergo} gr{\^a}ce {\`a} l'int{\'e}gration d'un solveur {SAT} efficace},
  author = {Coquereau, Albin},
  hal = {https://pastel.archives-ouvertes.fr/tel-02504894},
  number = {2019SACLY007},
  school = {Universit{\'e} Paris-Saclay},
  year = 2019,
  type = {Th{\`e}se de Doctorat}
}

@phdthesis{faissole19phd,
  topics = {team},
  title = {Formalisations d'analyses d'erreurs en analyse num{\'e}rique et en arithm{\'e}tique {\`a} virgule flottante},
  author = {Faissole, Florian},
  hal = {https://tel.archives-ouvertes.fr/tel-02470728},
  number = {2019SACLS594},
  school = {Universit{\'e} Paris Saclay},
  year = 2019,
  type = {Th{\`e}se de Doctorat}
}

@phdthesis{roux19phd,
  topics = {team},
  title = {Extensions de l'algorithme d'atteignabilit{\'e} arri{\`e}re dans le cadre de la v{\'e}rification de mod{\`e}les modulo th{\'e}ories},
  author = {Roux, Mattias},
  hal = {https://tel.archives-ouvertes.fr/tel-02496033},
  number = {2019SACLS582},
  school = {Universit{\'e} Paris Saclay},
  year = 2019,
  type = {Th{\`e}se de Doctorat}
}

@phdthesis{galloiswong21phd,
  topics = {team},
  title = {Formalisation en {Coq} des algorithmes de filtre num{\'e}rique calcul{\'e}s en pr{\'e}cision finie},
  author = {Gallois-Wong, Diane},
  hal = {https://tel.archives-ouvertes.fr/tel-03202580},
  number = {2021UPASG016},
  school = {Universit{\'e} Paris-Saclay},
  year = 2021,
  type = {Th{\`e}se de Doctorat}
}

@phdthesis{pascutto23phd,
  topics = {team},
  author = {Pascutto, Cl\'ement},
  title = {Runtime Verification of OCaml Programs},
  school = {Universit\'e Paris-Saclay},
  year = 2023,
  type = {PhD thesis}
}

@phdthesis{denis23phd,
  topics = {team},
  author = {Denis, Xavier},
  title = {Deductive Verification of Rust Programs},
  school = {Universit\'e Paris-Saclay},
  year = 2023,
  type = {PhD thesis}
}

@phdthesis{lanco23phd,
  topics = {team},
  author = {Lanco, Antoine},
  title = {Strat\'egies pour la r\'eduction forte},
  school = {Universit\'e Paris-Saclay},
  year = 2023,
  type = {PhD thesis}
}