David Pichardie
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
32
Venues
18
Active years
2004–2025
Best venue rank
A*
Where they publish
Papers
32 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | SAS | Contextual Equality Saturation. | Alexandre Drewery, Thomas P. Jensen, David Pichardie |
| 2022 | SAS | Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs. | Gilles Barthe, Adrien Koutsos, Solne Mirliaz, David Pichardie, Peter Schwabe |
| 2022 | VMCAI | A Flow-Insensitive-Complete Program Representation. | Solne Mirliaz, David Pichardie |
| 2021 | SAS | Verified Functional Programming of an Abstract Interpreter. | Lucas Franceschino, David Pichardie, Jean-Pierre Talpin |
| 2020 | CADE | A Fast Verified Liveness Analysis in SSA Form. | Jean-Christophe Lchenet, Sandrine Blazy, David Pichardie |
| 2018 | CC | Semantic reasoning about the sea of nodes. | Delphine Demange, Yon Fernndez de Retana, David Pichardie |
| 2018 | SAC | Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement. | Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie |
| 2017 | ESORICS | Verifying Constant-Time Implementations by Abstract Interpretation. | Sandrine Blazy, David Pichardie, Alix Trieu |
| 2017 | ITP | Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. | Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek |
| 2016 | ECOOP | An Extended Buffered Memory Model With Full Reorderings. | Gurvan Cabon, David Cachera, David Pichardie |
| 2016 | ICFP | An abstract memory functor for verified C static analyzers. | Sandrine Blazy, Vincent Laporte, David Pichardie |
| 2015 | CC | Verifying Fast and Sparse SSA-Based Optimizations in Coq. | Delphine Demange, David Pichardie, Lo Stefanesco |
| 2015 | CPP | Verified Validation of Program Slicing. | Sandrine Blazy, Andr Maroneze, David Pichardie |
| 2015 | ITP | Validating Dominator Trees for a Fast, Verified Dominance Test. | Sandrine Blazy, Delphine Demange, David Pichardie |
| 2015 | POPL | A Formally-Verified C Static Analyzer. | Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie |
| 2014 | CCS | System-level Non-interference for Constant-time Cryptography. | Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, David Pichardie |
| 2014 | ITP | Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. | Sandrine Blazy, Vincent Laporte, David Pichardie |
| 2014 | PLDI | Atomicity refinement for verified compilation. | Suresh Jagannathan, Gustavo Petri, Jan Vitek, David Pichardie, Vincent Laporte |
| 2014 | POPL | 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 |
| 2013 | POPL | Plan B: a buffered memory model for Java. | Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, Jan Vitek |
| 2013 | SAS | Formal Verification of a C Value Analysis Based on Abstract Interpretation. | Sandrine Blazy, Vincent Laporte, Andr Maroneze, David Pichardie |
| 2012 | ESOP | A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. | Gilles Barthe, Delphine Demange, David Pichardie |
| 2011 | CPP | Modular SMT Proofs for Fast Reflexive Checking Inside Coq. | Frdric Besson, Pierre-Emmanuel Cornilleau, David Pichardie |
| 2011 | ESOP | Secure the Clones - Static Enforcement of Policies for Secure Object Copying. | Thomas P. Jensen, Florent Kirchner, David Pichardie |
| 2010 | APLAS | A Provably Correct Stackless Intermediate Representation for Java Bytecode. | Delphine Demange, Thomas P. Jensen, David Pichardie |
| 2010 | ESORICS | Enforcing Secure Object Initialization in Java. | Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie |
| 2010 | ITP | A Certified Denotational Abstract Interpreter. | David Cachera, David Pichardie |
| 2008 | SEFM | Preservation of Proof Pbligations for Hybrid Verification Methods. | Gilles Barthe, Csar Kunz, David Pichardie, Julin Samborski-Forlese |
| 2007 | ESOP | A Certified Lightweight Non-interference Java Bytecode Verifier. | Gilles Barthe, David Pichardie, Tamara Rezk |
| 2006 | FLOPS | Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. | Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu |
| 2005 | FM | Certified Memory Usage Analysis. | David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider |
| 2004 | ESOP | Extracting a Data Flow Analyser in Constructive Logic. | David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu |