David Pichardie

David Pichardie is a Professor of Computer Science at ENS Rennes (France) and a Researcher at Meta. He holds a part-time teaching position at ENS Rennes while working on sabbatical leave. His research spans formal methods, programming languages, program verification, software security, and static analysis. He specializes in machine-checked proofs using Coq and abstract interpretation, with significant work on the verified C compiler CompCert. He has served on program committees for SAS, OOPSLA, POPL, and other leading conferences.

• Research Interests: Formal Methods, Static Analysis, Compiler Verification, Security, Abstract Interpretation, Programming Languages
• Awards: ERC Consolidator Grant (2018-2021)

His recent publications focus on verified JIT compilation, constant-time cryptography, SSA-based compiler optimizations, and concurrency verification. He has contributed to the formal verification of garbage collectors, WCET estimation tools, and information-flow architectures. His work often bridges theoretical formal verification with practical compiler design, emphasizing machine-checked proofs and integration into real-world systems like CompCert.

He has mentored students and collaborated on formal verification of Java bytecode, defensive copying policies, and static analysis of self-modifying code. His teaching includes courses on static analysis, formal methods, and algorithms at institutions such as University Rennes 1, INSA engineering school, and ENS Cachan.