About me


I am a research scientist at Inria Rennes, in the Celtique team (joint team between University of Rennes and ENS Cachan under the IRISA joint lab).
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 the INRIA Rennes research center in September 2007. 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...]


Contact

Address: INRIA, Projet Celtique, Campus de Beaulieu, 35042 Rennes Cedex France
E-mail: david[dot]pichardie[at]inria[dot]fr
Phone: +33 (0) 2 99 84 74 04
Fax: +33 (0) 2 99 84 71 71

Activities

News

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

[2012-2013] Sabbatical leave: I'm currently working at Harvard University with Prof. Greg Morrisett. This is a one year INRIA sabbatical leave.

[08/2012] Software: release of version 1.4 of the Sawja library ( Static Analysis Workshop for JAva) developed in the Celtique team.

[04/2012] Publication: Secure the Clones, with Thomas Jensen and Florent Kirchner, Logical Methods in Computer Science (LMCS), 8(2), 2012.

[12/2011] Publication: A formally verified SSA-based middle-end - Static Single Assignment meets CompCert, with Gilles Barthe and Delphine Demange, 21th European Symposium on Programming (ESOP 2012).

[09/2011] Publication: Modular SMT Proofs for Fast Reflexive Checking inside Coq, with Frédéric Besson and Pierre-Emmanuel Cornilleau 1st International Conference on Certified Programs and Proofs (CPP 2011).

Current research projects

  • VERASCO: french project (founded by ANR) about formal certification of compiler static analysis for C programs. (2012-2015)

Past research projects

  • Mobius: european project about Proof Carrying Code for Java on mobile devices (2005-2009).
  • ParSec: french project (founded by ANR) about secure concurrent programming (2006-2010).
  • ASCERT (principal investigator): french project (coordinator) (founded by FNRAE) about formal certification of static analyses. (2009-2012)
  • DECERT: french project (founded by ANR) about certifying decision procedures (2008-2011)
  • U3CAT: french project (founded by ANR) about the unification of critical C code analysis techniques inside the Frama-C platform (2008-2011).
  • CertLogs (principal investigator): french project founded by the Brittany region about software certificates (2009-2012).

Program committees

Lecturing