Sandrine Blazy
Thesis committees
2024
- Solène Mirliaz. Static relational cost analysis for superscalar architectures.
Ph.D. Rennes University. 16/12/2024. Advisor.
- Matthieu Baty. Formal verification of security mechanisms for the RISC-V ISA.
PhD. CentraleSupelec. 10/12/2024. President of jury.
- Thaïs Baudon. Algebraic data types for high-performance computing.
PhD. ENS de Lyon. 15/10/2024. President of jury.
- Nathanaëlle Courant. Towards an efficient and formally-verified convertibility checker.
PhD. Paris Cité University. 19/9/2024. Examiner.
- Henrik Plate. On the security risks of open source consumption.
PhD. Rennes University. 12/9/2024. President of jury.
- Quentin Le Dilavrec. Precise temporal analysis of source code histories at scale.
PhD. Rennes University. 5/2/2024. President of jury.
2023
- Enzo Crance. Meta-programming for proof transfer in dependent type theory.
PhD. Nantes University. 19/12/2023. Reviewer.
- Gautier Raimondi. Secure compilation against side-channel attacks.
Ph.D. Rennes University. 18/12/2023. President of jury.
- 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 Nron. 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.