Alix Trieu , since 2016.
Topic: Security enhancing compilation.
With David Pichardie.
Florent Saudel, since 2015.
Topic: vulnerability discovery.
With Frédéric Guihéry (Amossys).
David Bühler, since 2013.
Topic: Communication between analyses by deductive verification and
With Boris Yakobowski (CEA LIST).
Pierre Wilke, 2013-2016.
Topic: Low-level memory model for verified compilation.
With Frédéric Besson.
Vincent Laporte, 2012-2015.
Topic: Formal verification of static analyzers for low-level languages.
With David Pichardie. Now post-doc at IMDEA.
Stéphanie Riaud, 2011-2015.
Topic: Data obfuscation for protecting programs against dynamic
Now, engineer at DGA MI.
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.
Topic: Semantics of program obfuscation.
Topic: Verified bytecode compilation.
2014, with Delphine Demange.
Topic: Static analysis of binary code.
2012, with Frédéric Besson.
Topic: Static analysis of x86 assembly.
2011, with Guillaume Hiet and David Pichardie.
Topic: Java obfuscation techniques.
Topic: Introducing code obfuscation in a C compiler.
Topic: Formal verification of a register allocation algorithm. 2007,
with Éric Soutif.
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.
- Romain Vassallo.
Topic: Evolution of a program comprehension tool.
- Nathalie Dubois, Pousith Sayarath.
Topic: A pointer analysis for specializing Fortran programs.
- Frédéric Paumier, Hubert Parisot.
Topic: An interprocedural analysis for specializing Fortran programs.
- Skander Korrab.
Topic: Representing programs in the Centaur environment. 1993.