David Pichardie -

Registered user since Mon 18 Jul 2016

Name:David Pichardie

Country:France

Affiliation:Meta

Personal website:https://davidpichardie.github.io

Research interests:Machine-checked proofs, static analysis, programming languages, security

Contributions

POPL 2023	Author of Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler within the POPL-track Committee Member in Program Committee within the POPL-track Session Chair of Program Analysis & Parsing (part of POPL) Speaker of Program Analysis & Parsing: Session Preview within the Session Previews-track
SAS 2022	Author of Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs within the SAS-track
PLDI 2022	Author of (POPL 2021) Formally Verified Speculation and Deoptimization in a JIT Compiler within the SIGPLAN Track-track
VMCAI 2022	Author of A Flow-Insensitive-Complete Program Representation within the VMCAI 2022-track
PriSC 2022	Committee Member in Program Committee within the PriSC 2022-track
SAS 2021	Author of Verified Functional Programming of an Abstract Interpreter within the SAS-track Session Chair of Session 3C (part of SAS)
POPL 2021	Author of Formally Verified Speculation and Deoptimization in a JIT Compiler within the POPL-track
SAS 2020	Co-chair in Program Committee within the SAS-track Committee Member in Organizing Committee within the SAS-track Session Chair of 2 (part of SAS) Session Chair of 10 (part of SAS) General Co-Chair in Organizing Committee
CoqPL 2020	Author of Towards Formally Verified Just-in-Time compilation within the CoqPL-track
POPL 2020	Author of Formal Verification of a Constant-Time Preserving C Compiler within the Research Papers-track
PriSC 2020	Author of A CompCert Compiler that Preserves Cryptographic Constant-time within the Principles of Secure Compilation 2020-track
ECOOP and ISSTA 2018	Mentor in Mentors within the Summer School-track
CC 2017	Committee Member in Program Committee within the Research Papers-track
ICFP 2016	Author of An Abstract Memory Functor for Verified C Static Analyzers within the Research Papers-track
FTfJP 2016	Author of An Extended Buffered Memory Model With Full Reorderings within the FTfJP-track
VMCAI	Session Chair of Abstraction II (part of VMCAI)