I am professor of Computer Science at ENS Cachan, Brittany extension. My research activities take place in the Celtique team (joint team between University of Rennes and ENS Cachan under the IRISA joint lab, and Inria Rennes).
I received a Ph.D. in Computer Science from the University of Rennes, France, in 2005, and a Habilitation à diriger les recherches in Computer Science from the ENS Cachan, France, in 2012. I joined ENS Cachan in September 2013 as full professor. Between 2007 and 2013, I was a full research at INRIA Rennes research center. Earlier, I was holding a postdoc position at INRIA Sophia-Antipolis under the supervision of Gilles Barthe. In the 2011-13 academic years, I took a sabbatical and visited Jan Vitek's group at Purdue University, Indiana, USA, during the first year, and then Greg Morrisett's group at Harvard University, Cambridge, USA, during the second year.
My research interests include formal methods, programming languages, program verification, software, and system security. I am a long time happy user of the Coq proof assistant and the theory of Abstract interpretation. More recently I have been conducting several researches about the verified C compiler CompCert. [More...]
For research activities
|Address||:||INRIA, Projet Celtique|
|Campus de Beaulieu|
|35042 Rennes Cedex France|
|Phone||:||+33 (0) 2 99 84 22 59|
|Fax||:||+33 (0) 2 99 84 71 71|
For teaching activities
|Address||:||École normale supérieure de Cachan, Antenne de Bretagne|
|Campus de Ker Lann|
|35170 Bruz, France|
|Phone||:||+33 (0) 2 99 05 52 65|
|Fax||:||+33 (0) 2 99 05 93 28|
[10/2013] Publication: A Verified Information-Flow Architecture, with Arthur de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, Benjamin Pierce, Randy Pollack and Andrew Tolmach, 41th Symposium on Principles of Programming Languages (POPL 2014).
[09/2013] New position: I'm leaving my researcher position at Inria for a new full professor position at ENS Cachan, Brittany extension.
[04/2013] Publication: Formal Verification of Loop Bound Estimation for WCET Analysis, with Sandrine Blazy and André Maroneze, 5th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2013).
[03/2013] Publication: Formal Verification of a C Value Analysis Based on Abstract Interpretation, with Sandrine Blazy, Vincent Laporte and André Maroneze, 20th Static Analysis Symposium (SAS 2013).
[10/2012] Publication: Plan B: A Buffered Memory Model for Java, with Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan and Jan Vitek, 40th Symposium on Principles of Programming Languages (POPL 2013).
Current research projects
- VERASCO: french project (founded by ANR) about formal certification of compiler static analysis for C programs. (2012-2015)
- POPL 2015 (PC)
- ESOP 2014 (PC), FLoC 2014 (ITP workshop chair), ITP 2014 (PC)
- PLDI 2013 (ERC), BYTECODE 2013 (PC), ITP 2013 (co-chair), PxTP 2013 (PC), Coq Workshop 2013 (PC)
- IFM 2012 (PC), ITP 2012 (PC), PxTP 2012 (co-chair), SVARM & VERIFY 2012 (PC)
- JFLA 2011 (PC), BYTECODE 2011 (PC), PxTP 2011 (PC), PSATTT 2011 (PC), FoVeOOS 2011 (PC)
- BYTECODE 2010 (chair), ITP 2010 (PC), VERIFY 2010 (PC), IFM 2010 (PC)
- BYTECODE 2009 (PC), PCC 2009 (PC)
- NordSec'07 (PC)
- DigiCosme Spring School April 2013.
- University courses: I teach static analysis (2006-current) in the Master research of University Rennes 1 (co-responsible of the Component Based Embedded Software Track), Formal methods for software engineering (2007-2010) at INSA engineering school and Algorithms (2010) and Logic (2008-2009) at ENS Cachan, Brittany extension.
- FOSAD Summer School August, 2009
- Tutorial: Mobility, Ubiquity, and Security at ETAPS'07
- French summer school: EJCP'07
- Types Summer School August 19-31, 2007