David Pichardie

Publication Activity (10 Years)

Years Active: 2001-2023
Publications (10 Years): 25

Top Topics

Abstract Interpretation

Acid Properties

Top Venues

J. Autom. Reason.

Publications

Aurèle Barrière, Sandrine Blazy, David Pichardie
Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. Proc. ACM Program. Lang. 7 (POPL) (2023)
Ruba Mutasim, Gabriel Synnaeve, David Pichardie, Baptiste Rozière
Leveraging Static Analysis for Bug Repair. CoRR (2023)
Gilles Barthe, Adrien Koutsos, Solène Mirliaz, David Pichardie, Peter Schwabe
Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs. SAS (2022)
Solène Mirliaz, David Pichardie
A Flow-Insensitive-Complete Program Representation. VMCAI (2022)
Aurèle Barrière, Sandrine Blazy, David Pichardie
Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert Backend into a Formally Verified JIT Compiler. CoRR (2022)
Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie
Secure Compilation of Constant-Resource Programs. CSF (2021)
Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek
Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang. 5 (POPL) (2021)
Lucas Franceschino, David Pichardie, Jean-Pierre Talpin
Verified Functional Programming of an Abstract Interpreter. SAS (2021)
Lucas Franceschino, David Pichardie, Jean-Pierre Talpin
Verified Functional Programming of an Abstract Interpreter. CoRR (2021)
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4 (POPL) (2020)
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie
System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory. J. Autom. Reason. 64 (8) (2020)
Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie
A Fast Verified Liveness Analysis in SSA Form. IJCAR (2) (2020)
Sandrine Blazy, David Pichardie, Alix Trieu
Verifying constant-time implementations by abstract interpretation. J. Comput. Secur. 27 (1) (2019)
Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek
Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology. J. Autom. Reason. 63 (2) (2019)
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
Formal Verification of a Constant-Time Preserving C Compiler. IACR Cryptol. ePrint Arch. 2019 (2019)
Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie
Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement. SAC (2018)
David Pichardie, Mihaela Sighireanu
Preface. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 76 (2018)
Delphine Demange, Yon Fernández de Retana, David Pichardie
Semantic reasoning about the sea of nodes. CC (2018)
Sandrine Blazy, David Pichardie, Alix Trieu
Verifying Constant-Time Implementations by Abstract Interpretation. ESORICS (1) (2017)
Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek
Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. ITP (2017)
Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu
Verified Translation Validation of Static Analyses. CSF (2017)
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
A verified information-flow architecture. J. Comput. Secur. 24 (6) (2016)
Sandrine Blazy, Vincent Laporte, David Pichardie
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. J. Autom. Reason. 56 (3) (2016)
Gurvan Cabon, David Cachera, David Pichardie
An Extended Buffered Memory Model With Full Reorderings. FTfJP@ECOOP (2016)
Sandrine Blazy, Vincent Laporte, David Pichardie
An abstract memory functor for verified C static analyzers. ICFP (2016)
Sandrine Blazy, Delphine Demange, David Pichardie
Validating Dominator Trees for a Fast, Verified Dominance Test. ITP (2015)
Delphine Demange, David Pichardie, Léo Stefanesco
Verifying Fast and Sparse SSA-Based Optimizations in Coq. CC (2015)
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
A Verified Information-Flow Architecture. CoRR (2015)
Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie
A Formally-Verified C Static Analyzer. POPL (2015)
Sandrine Blazy, André Maroneze, David Pichardie
Verified Validation of Program Slicing. CPP (2015)
Suresh Jagannathan, Gustavo Petri, Jan Vitek, David Pichardie, Vincent Laporte
Atomicity refinement for verified compilation. PLDI (2014)
Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
A verified information-flow architecture. POPL (2014)
Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek
Atomicity Refinement for Verified Compilation. ACM Trans. Program. Lang. Syst. 36 (2) (2014)
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie
System-level non-interference for constant-time cryptography. IACR Cryptol. ePrint Arch. 2014 (2014)
Gilles Barthe, Delphine Demange, David Pichardie
Formal Verification of an SSA-Based Middle-End for CompCert. ACM Trans. Program. Lang. Syst. 36 (1) (2014)
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, David Pichardie
System-level Non-interference for Constant-time Cryptography. CCS (2014)
Sandrine Blazy, Vincent Laporte, David Pichardie
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. ITP (2014)
André Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut
A Formally Verified WCET Estimation Tool. WCET (2014)
Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
Formal Verification of a C Value Analysis Based on Abstract Interpretation. SAS (2013)
Gilles Barthe, David Pichardie, Tamara Rezk
A certified lightweight non-interference Java bytecode verifier. Math. Struct. Comput. Sci. 23 (5) (2013)
Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie
Formal Verification of a C Value Analysis Based on Abstract Interpretation CoRR (2013)
Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, Jan Vitek
Plan B: a buffered memory model for Java. POPL (2013)
Sandrine Blazy, André Maroneze, David Pichardie
Formal Verification of Loop Bound Estimation for WCET Analysis. VSTTE (2013)
Thomas P. Jensen, Florent Kirchner, David Pichardie
Secure the Clones Log. Methods Comput. Sci. 8 (2) (2012)
Gilles Barthe, Delphine Demange, David Pichardie
A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. ESOP (2012)
Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
Modular SMT Proofs for Fast Reflexive Checking Inside Coq. CPP (2011)
Thomas P. Jensen, Florent Kirchner, David Pichardie
Secure the Clones - Static Enforcement of Policies for Secure Object Copying. ESOP (2011)
David Cachera, David Pichardie
Programmation d'un interpréteur abstrait certifié en logique constructive. Tech. Sci. Informatiques 30 (4) (2011)
Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie
A Nelson-Oppen based Proof System using Theory Specific Proof Systems. PxTP (2011)
David Pichardie
Preface. Electron. Notes Theor. Comput. Sci. 264 (4) (2011)
Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie
Enforcing Secure Object Initialization in Java. ESORICS (2010)
Laurent Hubert, David Pichardie
Soundly Handling Static Fields: Issues, Semantics and Analysis CoRR (2010)
Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas P. Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
Sawja: Static Analysis Workshop for Java CoRR (2010)
Frédéric Besson, Guillaume Dufay, Thomas P. Jensen, David Pichardie
Verifying resource access control on mobile interactive devices. J. Comput. Secur. 18 (6) (2010)
Frédéric Besson, Thomas P. Jensen, David Pichardie, Tiphaine Turpin
Certified Result Checking for Polyhedral Analysis of Bytecode Programs. TGC (2010)
Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie
Enforcing Secure Object Initialization in Java CoRR (2010)
Delphine Demange, Thomas P. Jensen, David Pichardie
A Provably Correct Stackless Intermediate Representation for Java Bytecode. APLAS (2010)
Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas P. Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin
Sawja: Static Analysis Workshop for Java. FoVeOOS (2010)
David Cachera, David Pichardie
A Certified Denotational Abstract Interpreter. ITP (2010)
Frédéric Dabrowski, David Pichardie
A Certified Data Race Analysis for a Java-like Language. TPHOLs (2009)
Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie
Certified Static Analysis by Abstract Interpretation. FOSAD (2009)
Laurent Hubert, David Pichardie
Soundly Handling Static Fields: Issues, Semantics and Analysis. Electron. Notes Theor. Comput. Sci. 253 (5) (2009)
David Cachera, David Pichardie
Comparing Techniques for Certified Static Analysis. NASA Formal Methods (2009)
David Pichardie
Building Certified Static Analysers by Modular Construction of Well-founded Lattices. Electron. Notes Theor. Comput. Sci. 212 (2008)
Laurent Hubert, Thomas P. Jensen, David Pichardie
Semantic Foundations and Inference of Non-null Annotations. FMOODS (2008)
Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese
Preservation of Proof Pbligations for Hybrid Verification Methods. SEFM (2008)
Gilles Barthe, David Pichardie, Tamara Rezk
A Certified Lightweight Non-interference Java Bytecode Verifier. ESOP (2007)
Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie
The MOBIUS Proof Carrying Code Infrastructure. FMCO (2007)
Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. FLOPS (2006)
Frédéric Besson, Thomas P. Jensen, David Pichardie
Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. 364 (3) (2006)
David Pichardie
Modular Proof Principles for Parameterised Concretizations. CASSIS (2005)
David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider
Certified Memory Usage Analysis. FM (2005)
David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu
Extracting a data flow analyser in constructive logic. Theor. Comput. Sci. 342 (1) (2005)
David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu
Extracting a Data Flow Analyser in Constructive Logic. ESOP (2004)
Thomas Genet, Thomas P. Jensen, Vikash Kodati, David Pichardie
A Java Card CAP converter in PVS. Electron. Notes Theor. Comput. Sci. 82 (2) (2003)
David Cachera, David Pichardie
Embedding of Systems of Affine Recurrence Equations in Coq. TPHOLs (2003)
David Pichardie, Yves Bertot
Formalizing Convex Hull Algorithms. TPHOLs (2001)