Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, et al.. Formal verification of a constant-time preserving C compiler. Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩. ⟨hal-02975012⟩

Sandrine Blazy, David Pichardie, Alix Trieu. Verifying constant-time implementations by abstract interpretation. Journal of Computer Security, IOS Press, 2019, 27 (1), pp.137--163. ⟨10.3233/JCS-181136⟩. ⟨hal-02025047⟩

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, et al.. Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology. Journal of Automated Reasoning, Springer Verlag, 2018, ⟨10.1007/s10817-018-9489-x⟩. ⟨hal-01897251⟩

Arthur Azevedo de Amorim, Nathan Collins, André Dehon, Delphine Demange, Cătălin Hriţcu, et al.. A Verified Information-Flow Architecture. Journal of Computer Security, IOS Press, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩. ⟨hal-01424797⟩

Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. Journal of Automated Reasoning, Springer Verlag, 2016, 56 (3), pp.26. ⟨10.1007/s10817-015-9359-8⟩. ⟨hal-01243700⟩

Gilles Barthe, Delphine Demange, David Pichardie. Formal Verification of an SSA-based Middle-end for CompCert. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, 36 (1), pp.35. ⟨10.1145/2579080⟩. ⟨hal-01097677⟩

Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek. Atomicity Refinement for Verified Compilation. ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2014, pp.30. ⟨hal-01102435⟩

Gilles Barthe, David Pichardie, Tamara Rezk. A certified lightweight non-interference Java bytecode verifier. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23 (5), pp.1032-1081. ⟨10.1017/S0960129512000850⟩. ⟨hal-00915189⟩

Thomas Jensen, Florent Kirchner, David Pichardie. Secure the Clones. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (2). ⟨hal-00762377⟩

David Cachera, David Pichardie. Programmation d'un interpréteur abstrait certifié en logique constructive. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2011, pp.28. ⟨10.3166/tsi.30.381-408⟩. ⟨hal-01112680⟩

Frédéric Besson, Guillaume Dufaye, Thomas Jensen, David Pichardie. Verifying Resource Access Control on Mobile Interactive Devices. Journal of Computer Security, IOS Press, 2010, 18 (6), pp.971-998. ⟨inria-00537821⟩

Laurent Hubert, David Pichardie. Soundly Handling Static Fields: Issues, Semantics and Analysis. Electronic Notes in Theoretical Computer Science, Elsevier, 2009, Proceedings of the Fourth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2009), 253 (5), pp.15 - 30. ⟨10.1016/j.entcs.2009.11.012⟩. ⟨inria-00504028v2⟩

David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a data flow analyser in constructive logic. Theoretical Computer Science, Elsevier, 2005, 342 (1). ⟨inria-00564611⟩

Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie. A Fast Verified Liveness Analysis in SSA Form. IJCAR 2020- International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.324-340, ⟨10.1007/978-3-030-51054-1_19⟩. ⟨hal-02904204⟩

Delphine Demange, Yon Fernández de Retana, David Pichardie. Semantic reasoning about the sea of nodes. CC 2018 - 27th International Conference on Compiler Construction, Feb 2018, Vienna, Austria. pp.163-173, ⟨10.1145/3178372.3179503⟩. ⟨hal-01723236⟩

Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie. Verified Compilation of Linearizable Data Structures: Mechanizing Rely Guarantee for Semantic Refinement. SAC 2018 - The 33rd ACM/SIGAPP Symposium On Applied Computing, Apr 2018, Pau, France. pp.1881-1890, ⟨10.1145/3167132.3167333⟩. ⟨hal-01653620⟩

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, et al.. Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology. ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasília, Brazil. pp.496-513, ⟨10.1007/978-3-319-66107-0_31⟩. ⟨hal-01613389⟩

Sandrine Blazy, David Pichardie, Alix Trieu. Verifying Constant-Time Implementations by Abstract Interpretation. European Symposium on Research in Computer Security, Sep 2017, Oslo, Norway. ⟨hal-01588444⟩

Gurvan Cabon, David Cachera, David Pichardie. An Extended Buffered Memory Model With Full Reorderings. FtFjp - Ecoop workshop, Jul 2016, Rome, Italy. pp.1 - 6, ⟨10.1145/2955811.2955816⟩. ⟨hal-01379514⟩

Sandrine Blazy, Vincent Laporte, David Pichardie. An Abstract Memory Functor for Verified C Static Analyzers. ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. pp.14, ⟨10.1145/2951913.2951937⟩. ⟨hal-01339969⟩

Sandrine Blazy, Delphine Demange, David Pichardie. Validating Dominator Trees for a Fast, Verified Dominance Test. Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_6⟩. ⟨hal-01193281⟩

Delphine Demange, David Pichardie, Léo Stefanesco. Verifying Fast and Sparse SSA-based Optimizations in Coq.. 24th International Conference on Compiler Construction, CC 2015, 2015, London, United Kingdom. ⟨hal-01110779⟩

Sandrine Blazy, Andre Maroneze, David Pichardie. Verified Validation of Program Slicing. CPP 2015 : Conference on Certified Programs and Proofs, 2015, Mumbai, India. pp.109-117, ⟨10.1145/2676724.2693169⟩. ⟨hal-01110821⟩

Radoniaina Andriatsimandefitra Ratsisahanana, Thomas Genet, Laurent Guillo, Jean-François Lalande, David Pichardie, et al.. Kharon : Découvrir, comprendre et reconnaître des malware Android par suivi de flux d'information. Rendez-vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information, May 2015, Troyes, France. ⟨hal-01154368⟩

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie. A formally-verified C static analyzer. POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩. ⟨hal-01078386⟩

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie. System-level Non-interference for Constant-time Cryptography. ACM SIGSAC Conference on Computer and Communications Security, CCS'14, Nov 2014, Scottsdale, United States. pp.1267 - 1279, ⟨10.1145/2660267.2660283⟩. ⟨hal-01101950⟩

Arthur Azevedo de Amorim, Nathan Collins, André Dehon, Delphine Demange, Catalin Hritcu, et al.. A Verified Information-Flow Architecture. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. ⟨10.1145/2535838.2535839⟩. ⟨hal-00918847⟩

André Oliveira Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut. A Formally Verified WCET Estimation Tool. 14th International Workshop on Worst-Case Execution Time Analysis, Jul 2014, Madrid, Spain. ⟨10.4230/OASIcs.WCET.2014.11⟩. ⟨hal-01087194⟩

Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. The 5th International Conference on Interactive Theorem Proving (ITP 2014), 2014, Vienna, Austria. pp.128 - 143, ⟨10.1007/978-3-319-08970-6_9⟩. ⟨hal-01102445⟩

Delphine Demange, Vincent Laporte, Lei Zhao, David Pichardie, Suresh Jagannathan, et al.. Plan B: A Buffered Memory Model for Java. Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Jan 2013, Rome, Italy. ⟨hal-00924716⟩

Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344. ⟨hal-00812515⟩

Sandrine Blazy, André Maroneze, David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. VSTTE - Verified Software: Theories, Tools and Experiments, Natarajan Shankar, May 2013, Menlo Park, United States. pp.281-303. ⟨hal-00848703⟩

Gilles Barthe, Delphine Demange, David Pichardie. A Formally Verified SSA-based Middle-end: Static Single Assignment meets CompCert. 21th European Symposium on Programming, ESOP 2012, Mar 2012, Tallin, Estonia. pp.47-66, ⟨10.1007/978-3-642-28869-2_3⟩. ⟨hal-01110783⟩

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. Modular SMT Proofs for Fast Reflexive Checking inside Coq. First International Conference on Certified Programs and Proofs, 2011, Kenting, Taiwan. ⟨hal-00646960⟩

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. A Nelson-Oppen based Proof System using Theory Specific Proof Systems. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. ⟨hal-00677193⟩

Thomas Jensen, Florent Kirchner, David Pichardie. Secure the Clones - Static Enforcement of Policies for Secure Object Copying. ESOP 2011, 2011, Saarbrucken, Germany. ⟨hal-01110817⟩

Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin. Certified Result Checking for Polyhedral Analysis of Bytecode Programs. The 5th International Symposium on Trustworthy Global Computing (TGC), 2010, Munich, Germany. ⟨inria-00537816⟩

Guillaume Hiet, Frédéric Guihéry, Goulven Guiheux, David Pichardie, Christian Brunette. Sécurité de la plate-forme d'exécution Java : limites et propositions d'améliorations. Symposium sur la sécurité des technologies de l'information et des communications (SSTIC), 2010, Rennes, France. ⟨inria-00537820⟩

Laurent Hubert, Thomas Jensen, Vincent Monfort, David Pichardie. Enforcing Secure Object Initialization in Java. 15th European Symposium on Research in Computer Security (ESORICS), 2010, Athènes, Greece. pp.101-115. ⟨inria-00503953⟩

Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, et al.. Sawja: Static Analysis Workshop for Java. The International Conference on Formal Verification of Object-Oriented Software, Beckert, Bernhard and Marché, Claude, 2010, Paris, France. pp.253--267. ⟨inria-00504047⟩

Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation for Java Bytecode. The 8th Asian Symposium on Programming Languages and Systems (APLAS), 2010, Shangai, China. ⟨inria-00537815⟩

David Cachera, David Pichardie. A Certified Denotational Abstract Interpreter. International Conference on Interactive Theorem Proving (ITP), 2010, Edimburgh, United Kingdom. pp.9-24. ⟨inria-00537810⟩

Frédéric Dabrowski, David Pichardie. A Certified Data Race Analysis for a Java-like Language. TPHOL'09, 2009, Germany. pp.212--227. ⟨hal-00465547⟩

David Cachera, David Pichardie. Comparing Techniques for Certified Static Analysis. The NASA Formal Methods Symposium (NFM), 2009, Moffett Field, United States. pp.111-115. ⟨inria-00538772⟩

Frédéric Besson, David Cachera, Thomas Jensen, David Pichardie. Certified Static Analysis by Abstract Interpretation. Foundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. pp.223-257. ⟨inria-00538753⟩

David Pichardie. Building certified static analysers by modular construction of well-founded lattices. Proc. of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS'08), 2008, Shangai, China. ⟨inria-00332365⟩

Laurent Hubert, Thomas Jensen, David Pichardie. Semantic Foundations and Inference of Non-null Annotations. 10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), 2008, Oslo, Norway. ⟨inria-00332356⟩

Gilles Barthe, César Kunz, David Pichardie, Julian Samborski-Forlese. Preservation of proof obligations for hybrid verification methods. 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08), 2008, Cape Town, South Africa. ⟨inria-00332718⟩

Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu. Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. Functional and Logic Programming (FLOPS'06), 2006, Fuji Susono, Japan. ⟨inria-00564237⟩

David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. ESOP, 2004, Barcelona, Spain. ⟨inria-00564633⟩

David Pichardie, Yves Bertot. Formalizing Convex Hulls Algorithms. TPHOLs 2001 - 14th International Conference Theorem Proving in Higher Order Logics, Sep 2001, Edinburgh, United Kingdom. pp.346-361, ⟨10.1007/3-540-44755-5_24⟩. ⟨hal-01702679⟩

Sandrine Blazy, Christine Paulin-Mohring, David Pichardie. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David. Rennes, France. 7998, Springer, pp.500, 2013, Lecture Notes in Computer Science, ⟨10.1007/978-3-642-39634-2⟩. ⟨hal-00908865⟩

Gilles Barthe, David Pichardie, Tamara Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier. 2007. ⟨inria-00106182v2⟩

Solène Mirliaz, David Pichardie. Flow insensitive relational static analysis. [Intership report] ENS Rennes; Université Rennes 1. 2019. ⟨hal-02332139⟩

Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie. Compilation of Linearizable Data Structures: A Mechanised RG Logic for Semantic Refinement. [Research Report] ENS Rennes; IRISA, Inria Rennes; Université Rennes 1. 2017. ⟨hal-01538128⟩

Gilles Barthe, Delphine Demange, David Pichardie. Formal Verification of an SSA-based Middle-end for CompCert. [University works] 2011. ⟨inria-00634702v3⟩

Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation For Java Bytecode. [Research Report] RR-7021, INRIA. 2010, pp.59. ⟨inria-00414099v3⟩

Laurent Hubert, Thomas Jensen, David Pichardie. Semantic foundations and inference of non-null annotations. [Research Report] RR-6482, INRIA. 2008. ⟨inria-00266171v2⟩

Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin. Result certification for relational program analysis. [Research Report] RR-6333, INRIA. 2007, pp.32. ⟨inria-00166930v4⟩

David Pichardie, Vlad Rusu. Defining and Reasoning About General Recursive Functions in Type Theory: a Practical Method. [Research Report] PI 1766, 2005, pp.16. ⟨inria-00000910⟩

Frédéric Besson, Thomas Jensen, David Pichardie. A PCC Architecture based on Certified Abstract Interpretation. [Research Report] PI 1764, 2005, pp.35. ⟨inria-00000866⟩

Frédéric Besson, Thomas Jensen, David Pichardie. A PCC Architecture based on Certified Abstract Interpretation. [Research Report] RR-5751, INRIA. 2005, pp.35. ⟨inria-00070268⟩

David Pichardie. Toward a Verified Software Toolchain for Java. Computer Science [cs]. ENS Cachan, 2012. ⟨tel-01114001⟩