About me

I am professor of Computer Science and head of the Department of Computer Science at ENS Rennes. My research activities take place in the Celtique team (joint team between University of Rennes, ENS Rennes and Inria Rennes, under the IRISA joint lab).
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.

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
E-mail: david[dot]pichardie[at]irisa[dot]fr
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 Rennes
Campus de Ker Lann
35170 Bruz, France
E-mail: david[dot]pichardie[at]ens-rennes[dot]fr
Phone: +33 (0) 2 99 05 52 65
Fax: +33 (0) 2 99 05 93 28



[07/2014] Publication: System-level non-interference for constant-time cryptography, with Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, 21st Conference on Computer and Communications Security (CCS 2014).

[06/2014] Publication: A Formally Verified WCET Estimation Tool, with André Maronez, Sandrine Blazy and Isabelle Puaut, 14th International Workshop on Worst-Case Execution Time Analysis (WCET 2014).

[04/2014] Publication: Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code, with Sandrine Blazy and Vincent Laporte, 5th International Conference on Interactive Theorem Proving (ITP 2014).

[01/2014] Publication: Atomicity Refinement for Verified Compilation, with Suresh Jagannathan, Vincent Laporte, Gustavo Petri and Jan Vitek, ACM Trans. Program. Lang. Syst. (TOPLAS) (presented at PLDI'14).

[01/2014] Publication: Formal Verification of an SSA-Based Middle-End for CompCert, with Gilles Barthe and Delphine Demange, ACM Trans. Program. Lang. Syst. (TOPLAS).

[01/2014] New affiliation: The ENS Cachan, Brittany extension, is now a full ENS, the ENS Rennes.

[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)

Program committees