Sandrine Blazy
Ph.D.'s students
-
Clément Chavanon, since 2023.
Topic: refinement of formal specifications for trusted secure environments
With Frédéric Besson
-
Alain Delaët-Tixeuil, since 2022.
Topic: verified compilation for a language describing the law.
With Denis Merigoux.
-
Tony Law, since 2022.
Topic: verified compilation for high-level synthesis.
With Delphine Demange.
-
Roméo La Spina, since 2022.
Topic: Data-flow and dependency analysis for optimizing verified compilation.
With Delphine Demange.
-
Aurèle Barrière, 2019-2022.
Topic: Formal verification of JIT compilation.
With David Pichardie.
Now post-doc at EPFL.
-
Rémi Hutin, 2018-2021.
Topic: Verified secure compilation against timing side-channels.
With David Pichardie.
Now teacher assistant at ENS Rennes.
-
Alix Trieu, 2016-2018.
Topic: Verification of constant-time implementations in a verified compilation toolset.
With David Pichardie. Now, research engineer at ANSSI.
-
David Bühler, 2013-2016.
Topic: Structuring an abstract interpreter through value and state abstraction.
With Boris Yakobowski (CEA LIST).
Now, research engineer at CEA-LIST.
-
Pierre Wilke, 2013-2016.
Topic: Low-level memory model for verified compilation.
With Frédéric Besson. Now assistant professor at Centrale Supelec Rennes.
-
Vincent Laporte, 2012-2015.
Topic: Formal verification of static analyzers for low-level languages.
With David Pichardie. Now researcher at Inria.
-
Stéphanie Riaud, 2011-2015.
Topic: Data obfuscation for protecting programs against dynamic
analysis.
Now, engineer at DGA.
-
André Oliveira Maroneze, 2010-2014.
Topic: Verified compilation and WCET estimation.
With Isabelle Puaut and David Pichardie.
Now, research engineer at CEA-LIST.
-
Benoît Robillard, 2007-2010.
Topic: Formal verification and optimization of register allocation.
With Éric Soutif (CNAM). Now, engineer at Air France.
Master's interns
-
Roméo La Spina.
Topic: A dataflow analyser for CompCert, parameterized by an iteration order, with Delphine Demange.
2022
-
Aurèle Barrière.
Topic: Formal verification of JIT compilation.
2019.
-
Rémi Hutin.
Topic: Formal verification of program obfuscation.
2018.
-
Alix Trieu.
Topic: Formal verification of control-flow flattening.
2015.
-
Dorian Leroy.
Topic: Verified bytecode compilation.
2014, with Delphine Demange.
-
Joseph Afari.
Topic: Static analysis of binary code.
2012, with Frédéric Besson.
-
Vincent Laporte.
Topic: Static analysis of x86 assembly.
2011, with Guillaume Hiet and David Pichardie.
-
Hristo Hristov.
Topic: Java obfuscation techniques.
2011.
-
Stéphanie Riaud.
Topic: Introducing code obfuscation in a C compiler.
2011.
-
Benoît Robillard.
Topic: Formal verification of a register allocation algorithm. 2007,
with Éric Soutif.
-
Sonia Ksouri.
Topic: Separation logic and rely/guarantee. 2007, with Marc Shapiro.
-
Thomas Moniot. Topic: Formal semantics of a realistic subset of C. 2006.
- Maxime Bargiel.
Topic: automatic enrichment of formal glossaries. 2006, with Marc Frappier.
- Zaynah Dargaye.
Topic: Formal semantics and pre-compilation of a subset of C. 2005, with Xavier Leroy.
- Agnès Gonnet.
Topic: Validation in Coq of glossaries. 2005.
- François Armand. Topic: Certification in Coq of a compiler. 2004.
- Mourad Naouari.
Topic: Reverse-engineering of databases transactions. 2004, with Régine Laleau.
- Thibaut Tourneur. Topic: Data flow analysis certified in Coq. 2003.
- Nathalie Ly.
Topic: Implementation of mechanisms for reusing formal specification components.
2003, with Régine Laleau.
- Frédéric Gervais.
Topic: Reuse of formal specification components (in B).
2002, with Régine Laleau (LACL).
- Audrey Moulin.
Topic: Automating data migration programs.
1998.
- Romain Vassallo.
Topic: Evolution of a program comprehension tool.
1995.
- Nathalie Dubois, Pousith Sayarath.
Topic: A pointer analysis for specializing Fortran programs.
1995.
- Frédéric Paumier, Hubert Parisot.
Topic: An interprocedural analysis for specializing Fortran programs.
1994.
- Skander Korrab.
Topic: Representing programs in the Centaur environment. 1993.