About me

Mugshot


I am a research scientist at INRIA Rennes (IRISA), in the Celtique team.



My research area is about Proof Assistants (Coq, PVS) and Static Program Analysis (Abstract interpretation, Type systems, Proof Carrying Code). [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

[2011-2012] Sabbatical leave: I'm currently working at Purdue University with Prof. Jan Vitek. This is a one year INRIA sabbatical leave.

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

[06/2011] Software: release of version 1.3 of the Sawja library ( Static Analysis Workshop for JAva) developed in the Celtique team.

[12/2010] Publication: Secure the Clones: Static Enforcement of Policies for Secure Object Copying, with Thomas Jensen and Florent Kirchner, 20th European Symposium on Programming (ESOP 2011).

Current research projects

  • ASCERT: 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).

Program committees

Lecturing