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},
hal = {https://hal.science/tel-04696708},
author = {Pascutto, Cl\'ement},
title = {Runtime Verification of OCaml Programs},
school = {Universit\'e Paris-Saclay},
year = 2023,
type = {PhD thesis}
}
@phdthesis{denis23phd,
topics = {team},
hal = {https://hal.science/tel-04517581},
author = {Denis, Xavier},
title = {Deductive Verification of Rust Programs},
school = {Universit\'e Paris-Saclay},
year = 2023,
type = {PhD thesis}
}
@phdthesis{lanco23phd,
topics = {team},
hal = {https://hal.science/tel-04512443},
author = {Lanco, Antoine},
title = {Strat\'egies pour la r\'eduction forte},
school = {Universit\'e Paris-Saclay},
year = 2023,
type = {PhD thesis}
}
@phdthesis{mouhcine24phd,
topics = {team},
x-hal = {https://hal.science/tel-},
author = {Mouhcine, Houda},
title = {Formal Proofs in Applied Mathematics: A {Coq} Formalization
of Simplicial Lagrange Finite Elements},
school = {Universit\'e Paris-Saclay},
year = 2024,
type = {PhD thesis}
}
@phdthesis{andres24phd,
topics = {team},
x-hal = {https://hal.science/tel-},
author = {Andr{\`e}s, L{\'e}o},
title = {Exécution symbolique pour tous ou Compilation d’{OCaml} vers {WebAssembly}},
school = {Universit\'e Paris-Saclay},
year = 2024,
type = {PhD thesis}
}