About me


I am a researcher in the Meta company in Paris. I'm in sabbatical leave from my position of professor of Computer Science at ENS Rennes but I still hold a part-time teaching position there.
Mugshot
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 (in 2014, the brittany extension of ENS Cachan has becomed ENS Rennes). 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. From 2018 to 2021, my research has been funded by an ERC Consolidator Grant.
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. I have been conducting several researches about the verified C compiler CompCert in a recent past.


Contact

E-mail: david[dot]pichardie[at]ens-rennes[dot]fr

Activities

Program committees

Lecturing