Sandrine Blazy

• Home
• Publications
• Students
• Thesis Committees

Thesis committees

2023

• 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.

Page designed by Mike Cronin via OSWD