Thesis committees
2023
- Shenghao Yuan. Verified programming and secure integration of operating system libraries in Coq. Ph.D. Rennes University. 8/12/2023. President of jury.
- Swarn Priya. Formally computer-verified protections against timing-based side-channel attacks. PhD. University Côte d'Azur. 23/11/2023. Reviewer.
- Baptiste Pollien. Formal verification of an UAV autopilot: static analysis and verified code generation. PhD. University of Toulouse. 16/11/2023. Reviewer.
- Claire Maiza. Hardware and software analyses for precise and efficient timing analysis. HDR. University Grenoble Alpes. 9/6/2023. Reviewer.
- Arthur Charguéraud. A modern eye on separation logic for sequential programs. HDR. Strasbourg University. 27/02/2023. Examiner.
2022
- Aurèle Barrière. Formal verification of just-in-time compilation. Ph.D. Rennes 1 University. 14/12/2022. Advisor.
- Daniel De Almeida Braga. Cryptography in the wild: the security of cryptographic implementations. Ph.D. Rennes 1 University. 14/12/2022. President of jury.
- Adam Khayam. A meta-approach to describe effectful and distributed semantics. Ph.D. Rennes 1 University. 30/11/2022. President of jury.
- Jean-Joseph Marty. Verified information flow control applied to cyber-physical systems. Ph.D. Rennes 1 University. 17/11/2022. President of jury.
- Basile Clément. Translation validation of tensor compilers. Ph.D. ENS - Paris SL University. 09/09/2022. Examiner.
- Quentin Garchery. Certification of the transformation of proof tasks. Ph.D. University Paris Saclay. 25/01/2022. Reviewer.
2021
- Vincent Iampietro. Formal verification of a methodology for the design and production of safety-critical digital systems. Ph.D. University of Montpellier. 16/12/2021. Reviewer.
- Lucas Franceschino. Verified programming at the intersection of dependent types and static analysis. Ph.D. Rennes 1 University. 10/12/2021. President of jury.
- Rémi Hutin. Verified secure compilation against timing side-channels. Ph.D. Rennes 1 University. 1/12/2021. Advisor.
- Sylvain Boulmé. Formally-verified defensive programming. HDR. University Grenoble Alpes. 27/09/2021. Reviewer.
- Son Tuan Vu. Optimizing Property-Preserving Compilation. Ph.D. Sorbonne University. 2/4/2021. Examiner.
- Pierre-Évariste Dagand. The Usuba Experiment: Exploring Post-Moore Compilers. HDR. Sorbonne University. 26/03/2021. Reviewer.
2020
- Darius Mercadier. Usuba, optimizing bitslcing compiler. Ph.D. Sorbonne University. 20/11/2020. Reviewer.
- Charlie Jacomme. Proofs of security protocols - symbolic methods and powerful attackers. Ph.D. ENS Paris Saclay. 16/10/2020. Examiner.
- Cécile Baritel-Ruet. Formal security proofs of cryptographic ctandards - a necessity achieved using EasyCrypt. Ph.D. Côte d'Azur University. 28/10/2020. Reviewer.
2019
- Julien Lepiller. Verifying software fault isolation. Ph.D. Rennes 1 University. 11/12/2019. President of jury.
- Arif Ali Anapparakkal. Performance centric dynamic function level binary transformation. Ph.D. Rennes 1 University. 9/12/2019. President of jury.
- Yann Régis Gianas. About some Metamorphoses of Computer Programs. HDR. Paris University. 22/11/2019. Examiner.
- Matthieu Journault. Modular and precise static analysis by abstract interpretation for automatic proof of correct programs and contract inference. Ph.D. Paris Sorbonne University. 21/11/2019. Reviewer.
- Joseph Lallemand. Remote electronic voting: definitions and analysis techniques. Ph.D. Lorraine University. 08/11/2019. Examiner.
- Simon Lunel. A component-based approach to model and prove cyber-physical systems. Ph.D. Rennes 1 University. 28/01/2019. President of jury.
2018
- Rabab Bouziane. Software-level analysis and optimization to mitigate the cost of write operations on non-volatile memories. Ph.D. Rennes 1 University. 07/12/2018. President of jury.
- Alix Trieu. Verification of constant-time implementations in a certified compiler toolchain. Ph.D. Rennes 1 University. 04/12/2018. Advisor.
- Aurélie Hurault. Formalisations pour les compositions de services. HDR. Toulouse University. 07/08/2018. Examiner.
- Martin Clochard. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels. Ph.D. Paris Saclay University. 30/03/2018. Reviewer.
- Huisong Li. Shape abstractions with support for sharing and disjunctions. Ph.D. ENS - Paris SL University. 08/03/2018. President of jury.
2017
- Jordy Ruiz. Lookup of dataflow properties to improve worst-case execution time estimations. Ph.D. Toulouse University. 21/12/2017.
- Pierre Lestringant. Identification of cryptographic algorithms in native code. Ph.D. Rennes 1 University. 12/12/2017. President of jury.
- Alain Giorgetti. Specification and verification of parameterized systems. HDR. Franche-Conté University. 01/12/2017. Reviewer.
- Ninon Eyrolles. Obfuscation with mixed Boolean-arithmetic expressions: reconstruction, analysis and simplification tools. Ph.D. Paris-Saclay University. 30/06/2017. President of jury.
- Oana Andreescu. Static analysis of functional programs with an application to the frame problem in deductive verification. Ph.D. Rennes 1 University. 29/05/2017. President of jury.
- David Bühler. Structuring an abstract interpreter through value and state abstraction: EVA an evolved value analysis for Frama-C. Ph.D. Rennes 1 University. 15/03/2017. Advisor.
- Romain Aïssat. Infeasible path detection: a formal model and an algorithm. Ph.D. Paris-Saclay University. 30/01/2017. Reviewer.
2016
- Léon Gondelman. Un système de types pragmatique pour la vérification déductive de programmes. Ph.D. Paris-Saclay University. 13/12/2016. Reviewer.
- Thomas Degueule. Composition and interoperability for external domain-specific language engineering. Ph.D. Rennes 1 University. 12/12/2016. President of jury.
- Stefania-Gabriela Dumbrava. A Coq formalization of relational and deductive databases and mechanizations of Datalog. Ph.D. Paris-Saclay University. 2/12/2016. Reviewer.
- Pierre Wilke. Formally Verified Compilation of Low-Level Code. Ph.D. Rennes 1 University. 9/11/2016. Advisor.
- Arjun Suresh. Intercepting functions for memoisation. Ph.D. Rennes 1 University. 10/5/2016. President of jury.
2015
- Stéphanie Riaud. Obfuscation de données pour la protection de programmes contre l'analyse dynamique. Ph.D. Rennes 1 University. 14/12/2015. Advisor.
- Lourdes del Carmen Gonzalez Huesca. Incrementality and effect simulation in the simply typed lambda calculus. Ph.D. Paris Diderot University. 27/11/2015. Examiner.
- Vincent Laporte. Verification of static analysis for low-level languages. Ph.D. Rennes 1 University. 25/11/2015. Advisor.
- Zakaria Chihani. Certification of first-order proofs in classical and intuitionistic logics. Ph.D. École Polytechnique. 2/11/2015. Examiner.
- Alexis Fouilhé. Revisiting the abstract domain of polyhedra: constraints only representation and formal proof. Ph.D. University of Grenoble. 15/10/2015. Examiner.
2014
- Étienne Millon. Analyse de sécurité de logiciels système par typage statique - Application au noyau Linux. Ph.D. Paris 6 University. 10/07/2014. Reviewer.
- Van Chan Ngo. Formal verification of a synchronous data-flow compiler: from Signal to C. Ph.D. Rennes 1 University. 1/07/2014. President of jury.
- André Oliveira Maroneze. Verified compilation and worst-case estimation time estimation. Ph.D. Rennes 1 University. 17/06/2014. Advisor.
- Vincent Benayoun. Analyse de dépendances ML pour les évaluateurs critiques. Ph.D. CNAM. 16/05/2014. Reviewer.
2013
- Jean Fortin. BSP-Why: a tool for deductive program verification of BSP programs. Ph.D. University Paris East. 14/10/2013. Reviewer.
- Pierre Néron. A quest for exactness: program transformation for reliable real numbers. Ph.D. École Polytechnique. 4/10/2013. Examiner.
- Xiaomu Shi. Certification of an instruction set simulator. Ph.D. Grenoble University. 10/07/2013. Reviewer.
- Benjamin Lesage. Architecture multi-coeurs et temps d'exécution au pire cas. Ph.D. Rennes 1 University. 21/05/2013. President of jury.
- Suman Saha. Improving the Quality of Error-Handling Code in Systems Software using Function-Local Information. Ph.D. University Paris 6. 25/03/2013. Reviewer.
- Cédric Auger. Certified compilation of SCADE/LUSTRE. Ph.D. University Paris Sud. 07/02/2013. Reviewer.
2012
- Vincent Filou. Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant à la preuve Coq. Ph.D. University of Bordeaux. 14/12/2012. Reviewer.
- Eric Totel. Techniques de détection d'erreur appliquées à la détection d'intrusion. HDR. Rennes 1 University. 6/12/2012. Examiner.
- Etienne Lozes. Separation Logic: Expressiveness and Copyless Message-Passing. HDR. ENS Cachan. 06/07/2012. Reviewer.
- Ricardo Bedin Franca. Ph.D. Toulouse University. 10/04/2012. Examiner.
2011
- François Bobot. Logique de séparation et vérification déductive. Ph.D. University Paris Sud. 12/12/2011. Reviewer.
- Philippe Beaucamps. Analyse de programmes malveillants par abstraction de comportements. Ph.D. Nancy University. 03/10/2011. Reviewer.
- Nassima Izerrouken. Développement prouvé de composants formels pour un générateur de code embarqué critique pré-qualifié. Ph.D. Toulouse University. 07/07/2011. Reviewer.
- Alan Schmitt. Static analyses for manipulations of hierarchically structured data. HDR. Grenoble University. 05/2011. Reviewer.
2010
- Benoît Robillard. Formal verification and optimization of register allocation. Ph.D. CNAM. 23/11/2010. Advisor.