Formalizing Convex Hull Algorithms. - David Pichardie; Yves Bertot (TPHOLs, 2001)

Embedding of Systems of Affine Recurrence Equations in Coq. - David Cachera; David Pichardie (TPHOLs, 2003)

A Java Card CAP converter in PVS. - Thomas Genet; Thomas P. Jensen; Vikash Kodati; David Pichardie (COCV@ETAPS, 2003)

Modular Proof Principles for Parameterised Concretizations. - David Pichardie (CASSIS, 2005)

Certified Memory Usage Analysis. - David Cachera; Thomas P. Jensen; David Pichardie; Gerardo Schneider (FM, 2005)

Extracting a data flow analyser in constructive logic. - David Cachera; Thomas P. Jensen; David Pichardie; Vlad Rusu (Theor. Comput. Sci., 2005)

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. - Gilles Barthe; Julien Forest; David Pichardie; Vlad Rusu (FLOPS, 2006)

Proof-carrying code from certified abstract interpretation and fixpoint compression. - Frédéric Besson; Thomas P. Jensen; David Pichardie (Theor. Comput. Sci., 2006)

The MOBIUS Proof Carrying Code Infrastructure. - Gilles Barthe; Pierre Crégut; Benjamin Grégoire; Thomas P. Jensen; David Pichardie (FMCO, 2007)

Semantic Foundations and Inference of Non-null Annotations. - Laurent Hubert; Thomas P. Jensen; David Pichardie (FMOODS, 2008)

Preservation of Proof Pbligations for Hybrid Verification Methods. - Gilles Barthe; César Kunz; David Pichardie; Julián Samborski-Forlese (SEFM, 2008)

Building Certified Static Analysers by Modular Construction of Well-founded Lattices. - David Pichardie (FICS, 2008)

Certified Static Analysis by Abstract Interpretation. - Frédéric Besson; David Cachera; Thomas P. Jensen; David Pichardie (FOSAD, 2009)

Comparing Techniques for Certified Static Analysis. - David Cachera; David Pichardie (NASA Formal Methods, 2009)

A Certified Data Race Analysis for a Java-like Language. - Frédéric Dabrowski; David Pichardie (TPHOLs, 2009)

Soundly Handling Static Fields: Issues, Semantics and Analysis. - Laurent Hubert; David Pichardie (BYTECODE@ETAPS, 2009)

A Provably Correct Stackless Intermediate Representation for Java Bytecode. - Delphine Demange; Thomas P. Jensen; David Pichardie (APLAS, 2010)

Enforcing Secure Object Initialization in Java. - Laurent Hubert; Thomas P. Jensen; Vincent Monfort; David Pichardie (ESORICS, 2010)

Sawja: Static Analysis Workshop for Java. - Laurent Hubert; Nicolas Barré; Frédéric Besson; Delphine Demange; Thomas P. Jensen; Vincent Monfort; David Pichardie; Tiphaine Turpin (FoVeOOS, 2010)

A Certified Denotational Abstract Interpreter. - David Cachera; David Pichardie (ITP, 2010)

Certified Result Checking for Polyhedral Analysis of Bytecode Programs. - Frédéric Besson; Thomas P. Jensen; David Pichardie; Tiphaine Turpin (TGC, 2010)

Preface. - David Pichardie (Bytecode@ETAPS, 2010)

Verifying resource access control on mobile interactive devices. - Frédéric Besson; Guillaume Dufay; Thomas P. Jensen; David Pichardie (J. Comput. Secur., 2010)

Modular SMT Proofs for Fast Reflexive Checking Inside Coq. - Frédéric Besson; Pierre-Emmanuel Cornilleau; David Pichardie (CPP, 2011)

Secure the Clones - Static Enforcement of Policies for Secure Object Copying. - Thomas P. Jensen; Florent Kirchner; David Pichardie (ESOP, 2011)

A Nelson-Oppen based Proof System using Theory Specific Proof Systems. - Frédéric Besson; Pierre-Emmanuel Cornilleau; David Pichardie (PxTP, 2011)

Programmation d'un interpréteur abstrait certifié en logique constructive. - David Cachera; David Pichardie (Tech. Sci. Informatiques, 2011)

Toward a Verified Software Toolchain for Java. - David Pichardie (2012)

A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. - Gilles Barthe; Delphine Demange; David Pichardie (ESOP, 2012)

Secure the Clones - Thomas P. Jensen; Florent Kirchner; David Pichardie (Log. Methods Comput. Sci., 2012)

Plan B: a buffered memory model for Java. - Delphine Demange; Vincent Laporte; Lei Zhao; Suresh Jagannathan; David Pichardie; Jan Vitek (POPL, 2013)

Formal Verification of a C Value Analysis Based on Abstract Interpretation. - Sandrine Blazy; Vincent Laporte; André Maroneze; David Pichardie (SAS, 2013)

Formal Verification of Loop Bound Estimation for WCET Analysis. - Sandrine Blazy; André Maroneze; David Pichardie (VSTTE, 2013)

A certified lightweight non-interference Java bytecode verifier. - Gilles Barthe; David Pichardie; Tamara Rezk (Math. Struct. Comput. Sci., 2013)

A Formally Verified WCET Estimation Tool. - André Maroneze; Sandrine Blazy; David Pichardie; Isabelle Puaut (WCET, 2014)

System-level non-interference for constant-time cryptography. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001; David Pichardie (IACR Cryptol. ePrint Arch., 2014)

Formal Verification of an SSA-Based Middle-End for CompCert. - Gilles Barthe; Delphine Demange; David Pichardie (ACM Trans. Program. Lang. Syst., 2014)

Atomicity Refinement for Verified Compilation. - Suresh Jagannathan; Vincent Laporte; Gustavo Petri; David Pichardie; Jan Vitek (ACM Trans. Program. Lang. Syst., 2014)

Verifying Fast and Sparse SSA-Based Optimizations in Coq. - Delphine Demange; David Pichardie; Léo Stefanesco (CC, 2015)

Verified Validation of Program Slicing. - Sandrine Blazy; André Maroneze; David Pichardie (CPP, 2015)

Validating Dominator Trees for a Fast, Verified Dominance Test. - Sandrine Blazy; Delphine Demange; David Pichardie (ITP, 2015)

A Formally-Verified C Static Analyzer. - Jacques-Henri Jourdan; Vincent Laporte; Sandrine Blazy; Xavier Leroy; David Pichardie (POPL, 2015)

An Extended Buffered Memory Model With Full Reorderings. - Gurvan Cabon; David Cachera; David Pichardie (FTfJP@ECOOP, 2016)

An abstract memory functor for verified C static analyzers. - Sandrine Blazy; Vincent Laporte; David Pichardie (ICFP, 2016)

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. - Sandrine Blazy; Vincent Laporte; David Pichardie (J. Autom. Reason., 2016)

A verified information-flow architecture. - Arthur Azevedo de Amorim; Nathan Collins; André DeHon; Delphine Demange; Catalin Hritcu; David Pichardie; Benjamin C. Pierce; Randy Pollack; Andrew Tolmach (J. Comput. Secur., 2016)

Verified Translation Validation of Static Analyses. - Gilles Barthe; Sandrine Blazy; Vincent Laporte; David Pichardie; Alix Trieu (CSF, 2017)

Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. - Yannick Zakowski; David Cachera; Delphine Demange; Gustavo Petri; David Pichardie; Suresh Jagannathan; Jan Vitek (ITP, 2017)

Semantic reasoning about the sea of nodes. - Delphine Demange; Yon Fernández de Retana; David Pichardie (CC, 2018)

Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement. - Yannick Zakowski; David Cachera; Delphine Demange; David Pichardie (SAC, 2018)

Preface. - David Pichardie; Mihaela Sighireanu (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2018)

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology. - Yannick Zakowski; David Cachera; Delphine Demange; Gustavo Petri; David Pichardie; Suresh Jagannathan; Jan Vitek (J. Autom. Reason., 2019)

Verifying constant-time implementations by abstract interpretation. - Sandrine Blazy; David Pichardie; Alix Trieu (J. Comput. Secur., 2019)

A Fast Verified Liveness Analysis in SSA Form. - Jean-Christophe Léchenet; Sandrine Blazy; David Pichardie (IJCAR (2), 2020)

System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001; David Pichardie (J. Autom. Reason., 2020)

Formal verification of a constant-time preserving C compiler. - Gilles Barthe; Sandrine Blazy; Benjamin Grégoire; Rémi Hutin; Vincent Laporte; David Pichardie; Alix Trieu (Proc. ACM Program. Lang., 2020)

Secure Compilation of Constant-Resource Programs. - Gilles Barthe; Sandrine Blazy; Rémi Hutin; David Pichardie (CSF, 2021)

Verified Functional Programming of an Abstract Interpreter. - Lucas Franceschino; David Pichardie; Jean-Pierre Talpin (SAS, 2021)

Formally verified speculation and deoptimization in a JIT compiler. - Aurèle Barrière; Sandrine Blazy; Olivier Flückiger; David Pichardie; Jan Vitek (Proc. ACM Program. Lang., 2021)

Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs. - Gilles Barthe; Adrien Koutsos; Solène Mirliaz; David Pichardie; Peter Schwabe (SAS, 2022)

A Flow-Insensitive-Complete Program Representation. - Solène Mirliaz; David Pichardie (VMCAI, 2022)

Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert Backend into a Formally Verified JIT Compiler. - Aurèle Barrière; Sandrine Blazy; David Pichardie (CoRR, 2022)

Leveraging Static Analysis for Bug Repair. - Ruba Mutasim; Gabriel Synnaeve; David Pichardie; Baptiste Rozière (CoRR, 2023)

Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. - Aurèle Barrière; Sandrine Blazy; David Pichardie (Proc. ACM Program. Lang., 2023)

Preface of the special issue on the static analysis symposium 2020 and 2022. - David Pichardie; Mihaela Sighireanu; Gagandeep Singh 001; Caterina Urban (Formal Methods Syst. Des., 2025)