[36] Guillaume Melquiond. Formal Verification for Numerical Computations, and the Other Way Around. Habilitation à diriger des recherches, Université Paris Sud, April 2019. [ bib | full text on HAL ]
[35] Mário Pereira. Tools and Techniques for the Verification of Modular Stateful Code. Thèse de doctorat, Université Paris-Saclay, December 2018. [ bib ]
[34] David Declerck. Verification via Model Checking of Parameterized Concurrent Programs on Weak Memory Models. Thèse de doctorat, Université Paris-Saclay, September 2018. [ bib | full text on HAL ]
Keywords: Weak memory ; Model checking ; Verification ; Mémoire faible
[33] Martin Clochard. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels. Thèse de doctorat, Université Paris-Saclay, March 2018. [ bib | full text on HAL ]
[32] Léon Gondelman. A Pragmatic Type System for Deductive Software Verification. Thèse de doctorat, Université Paris-Saclay, 2016. [ bib | full text on HAL ]
[31] Catherine Lelay. Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée. Thèse de doctorat, Université Paris-Sud, June 2015. [ bib | full text on HAL ]
[30] Sylvie Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Thèse d'habilitation, Université Paris-Sud, October 2014. [ bib | full text on HAL ]
[29] Alain Mebsout. Invariants inference for model checking of parameterized systems. Thèse de doctorat, Université Paris-Sud, September 2014. [ bib | full text on HAL ]
[28] Évelyne Contejean. Facettes de la preuve, Jeux de reflets entre démonstration automatique et preuve assisté. Thèse d'habilitation, Université Paris-Sud, June 2014. https://www.lri.fr/~contejea/dossiers/hdr/hdr.pdf. [ bib | full text on HAL ]
[27] Claire Dross. Generic Decision Procedures for Axiomatic First-Order Theories. Thèse de doctorat, Université Paris-Sud, April 2014. [ bib | full text on HAL ]
[26] Asma Tafat. Preuves par raffinement de programmes avec pointeurs. Thèse de doctorat, Université Paris-Sud, September 2013. [ bib | full text on HAL ]
[25] Mohamed Iguernelala. Strengthening the Heart of an SMT-Solver: Design and Implementation of Efficient Decision Procedures. Thèse de doctorat, Université Paris-Sud, June 2013. [ bib | full text on HAL ]
[24] Cédric Auger. Compilation Certifiée de SCADE/LUSTRE. Thèse de doctorat, Université Paris-Sud, February 2013. http://tel.archives-ouvertes.fr/tel-00818169/. [ bib | full text on HAL ]
[23] Paolo Herms. Certification of a Tool Chain for Deductive Program Verification. Thèse de doctorat, Université Paris-Sud, January 2013. http://tel.archives-ouvertes.fr/tel-00789543. [ bib | full text on HAL ]
[22] Sylvain Conchon. SMT Techniques and their Applications: from Alt-Ergo to Cubicle. Thèse d'habilitation, Université Paris-Sud, December 2012. In English, http://www.lri.fr/~conchon/publis/conchonHDR.pdf. [ bib | .html ]
[21] Thi Minh Tuyen Nguyen. Taking architecture and compiler into account in formal proofs of numerical programs. Thèse de doctorat, Université Paris-Sud, June 2012. [ bib | full text on HAL | .pdf ]
[20] François Bobot. Logique de séparation et vérification déductive. Thèse de doctorat, Université Paris-Sud, December 2011. [ bib | full text on HAL | .pdf ]
[19] Jean-Christophe Filliâtre. Deductive Program Verification. Thèse d'habilitation, Université Paris-Sud, December 2011. [ bib | .pdf ]
[18] Romain Bardou. Verification of Pointer Programs Using Regions and Permissions. Thèse de doctorat, Université Paris-Sud, October 2011. http://proval.lri.fr/publications/bardou11phd.pdf. [ bib | full text on HAL | .pdf ]
[17] Stéphane Lescuyer. Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq. Thèse de doctorat, Université Paris-Sud, January 2011. [ bib | full text on HAL | .pdf ]
[16] Xavier Urbain. Preuve automatique : techniques, outils et certification. Thèse d'habilitation, Université Paris-Sud 11, November 2010. [ bib ]
[15] Florence Plateau. Modèle n-synchrone pour la programmation de réseaux de Kahn à mémoire bornée. Thèse de doctorat, Université Paris-Sud, 2010. [ bib ]
[14] Johannes Kanig. Spécification et preuve de programmes d'ordre supérieur. Thèse de doctorat, Université Paris-Sud, 2010. [ bib ]
[13] Yannick Moy. Automatic Modular Static Safety Checking for C Programs. PhD thesis, Université Paris-Sud, January 2009. [ bib | .pdf ]
[12] Matthieu Sozeau. Un environnement pour la programmation avec types dépendants. Thèse de doctorat, Université Paris-Sud, December 2008. [ bib ]
[11] Thierry Hubert. Analyse Statique et preuve de Programmes Industriels Critiques. Thèse de doctorat, Université Paris-Sud, June 2008. [ bib | .pdf ]
[10] Nicolas Rousset. Automatisation de la Spécification et de la Vérification d'applications Java Card. Thèse de doctorat, Université Paris-Sud, June 2008. [ bib | .pdf ]
[9] Nicolas Oury. Égalités et filtrages avec types dépendants dans le Calcul des Constructions Inductives. Thèse de doctorat, Université Paris-Sud, September 2006. [ bib ]
[8] Julien Signoles. Extension de ML avec raffinement : syntaxe, sémantiques et système de types. Thèse de doctorat, Université Paris-Sud, July 2006. [ bib ]
[7] June Andronick. Modélisation et vérification formelles de systèmes embarqués dans les cartes à microprocessur. Plateforme Java Card et Système d'exploitation. Thèse de doctorat, Université Paris-Sud, March 2006. [ bib ]
[6] Louis Mandel. Conception, Sémantique et Implantation de ReactiveML : un langage à la ML pour la programmation réactive. PhD thesis, Université Paris 6, 2006. [ bib | PDF | .pdf ]
[5] Claude Marché. Preuves mécanisées de Propriétés de Programmes. Thèse d'habilitation, Université Paris 11, December 2005. [ bib | .pdf ]
[4] Pierre Corbineau. Démonstration Automatique en Théorie des Types. Thèse de doctorat, Université Paris-Sud, September 2005. [ bib ]
[3] Pierre Letouzey. Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. Thèse de doctorat, Université Paris-Sud, July 2004. [ bib | .ps.gz ]
[2] Jacek Chrzaszcz. Modules in Type Theory with Generative Definitions. PhD thesis, Warsaw University, Poland and Université de Paris-Sud, January 2004. [ bib ]
[1] Mihai Rotaru. Sur une théorie unificatrice des modèles de concurrence. PhD thesis, Cluj University, Romania and Université de Paris-Sud, January 2004. [ bib ]