Accéder directement au contenu

David Pichardie

69
Documents

Publications

Image document

Formally verified speculation and deoptimization in a JIT compiler

Aurèle Barrière , Sandrine Blazy , Olivier Flückiger , David Pichardie , Jan Vitek
Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.26. ⟨10.1145/3434327⟩
Article dans une revue hal-03185848v1
Image document

Formal verification of a constant-time preserving C compiler

Gilles Barthe , Sandrine Blazy , Benjamin Grégoire , Rémi Hutin , Vincent Laporte
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩
Article dans une revue hal-02975012v1
Image document

Verifying constant-time implementations by abstract interpretation

Sandrine Blazy , David Pichardie , Alix Trieu
Journal of Computer Security, 2019, 27 (1), pp.137--163. ⟨10.3233/JCS-181136⟩
Article dans une revue hal-02025047v1
Image document

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology

Yannick Zakowski , David Cachera , Delphine Demange , Gustavo Petri , David Pichardie
Journal of Automated Reasoning, 2018, ⟨10.1007/s10817-018-9489-x⟩
Article dans une revue hal-01897251v1
Image document

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code

Sandrine Blazy , Vincent Laporte , David Pichardie
Journal of Automated Reasoning, 2016, 56 (3), pp.26. ⟨10.1007/s10817-015-9359-8⟩
Article dans une revue hal-01243700v1

A Verified Information-Flow Architecture

Arthur Azevedo de Amorim , Nathan Collins , André Dehon , Delphine Demange , Cătălin Hriţcu
Journal of Computer Security, 2016, 24 (6), pp.689--734. ⟨10.3233/JCS-15784⟩
Article dans une revue hal-01424797v1

Formal Verification of an SSA-based Middle-end for CompCert

Gilles Barthe , Delphine Demange , David Pichardie
ACM Transactions on Programming Languages and Systems (TOPLAS), 2014, 36 (1), pp.35. ⟨10.1145/2579080⟩
Article dans une revue hal-01097677v1

Atomicity Refinement for Verified Compilation

Suresh Jagannathan , Vincent Laporte , Gustavo Petri , David Pichardie , Jan Vitek
ACM Transactions on Programming Languages and Systems (TOPLAS), 2014, pp.30
Article dans une revue hal-01102435v1
Image document

A certified lightweight non-interference Java bytecode verifier

Gilles Barthe , David Pichardie , Tamara Rezk
Mathematical Structures in Computer Science, 2013, 23 (5), pp.1032-1081. ⟨10.1017/S0960129512000850⟩
Article dans une revue hal-00915189v1
Image document

Secure the Clones

Thomas Jensen , Florent Kirchner , David Pichardie
Logical Methods in Computer Science, 2012, 8 (2)
Article dans une revue hal-00762377v1

Programmation d'un interpréteur abstrait certifié en logique constructive

David Cachera , David Pichardie
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2011, pp.28. ⟨10.3166/tsi.30.381-408⟩
Article dans une revue hal-01112680v1
Image document

Verifying Resource Access Control on Mobile Interactive Devices

Frédéric Besson , Guillaume Dufaye , Thomas Jensen , David Pichardie
Journal of Computer Security, 2010, 18 (6), pp.971-998
Article dans une revue inria-00537821v1
Image document

Soundly Handling Static Fields: Issues, Semantics and Analysis

Laurent Hubert , David Pichardie
Electronic Notes in Theoretical Computer Science, 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⟩
Article dans une revue inria-00504028v2
Image document

Extracting a data flow analyser in constructive logic

David Cachera , Thomas Jensen , David Pichardie , Vlad Rusu
Theoretical Computer Science, 2005, 342 (1), pp.56-78. ⟨10.1016/j.tcs.2005.06.004⟩
Article dans une revue inria-00564611v1
Image document

Semantic foundations for cost analysis of pipeline-optimized programs

Gilles Barthe , Adrien Koutsos , Solène Mirliaz , David Pichardie , Peter Schwabe
SAS 2022 - 29th International Symposium on Static Analysis, Dec 2022, Auckland, New Zealand. ⟨10.1007/978-3-031-22308-2_17⟩
Communication dans un congrès hal-03779257v1
Image document

A Flow-Insensitive-Complete Program Representation

Solène Mirliaz , David Pichardie
23rd International Conference Verification, Model Checking, and Abstract Interpretation (VMCAI 2022 ), Jan 2022, Philadelphia, United States. ⟨10.1007/978-3-030-94583-1_10⟩
Communication dans un congrès hal-04273047v1
Image document

Verified Functional Programming of an Abstract Interpreter

Lucas Franceschino , Jean-Pierre Talpin , David Pichardie
SAS 2021 - 28th Static Analysis Symposium, Oct 2021, Chicago, United States. pp.1-20
Communication dans un congrès hal-03342997v1
Image document

Secure Compilation of Constant-Resource Programs

Gilles Barthe , Sandrine Blazy , Rémi Hutin , David Pichardie
CSF 2021 - 34th IEEE Computer Security Foundations Symposium, Jun 2021, Dubrovnik, Croatia. pp.1-12
Communication dans un congrès hal-03221440v1
Image document

A Fast Verified Liveness Analysis in SSA Form

Jean-Christophe Léchenet , Sandrine Blazy , David Pichardie
IJCAR 2020- International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.324-340, ⟨10.1007/978-3-030-51054-1_19⟩
Communication dans un congrès hal-02904204v1
Image document

Semantic reasoning about the sea of nodes

Delphine Demange , Yon Fernández de Retana , David Pichardie
CC 2018 - 27th International Conference on Compiler Construction, Feb 2018, Vienna, Austria. pp.163-173, ⟨10.1145/3178372.3179503⟩
Communication dans un congrès hal-01723236v1
Image document

Verified Compilation of Linearizable Data Structures: Mechanizing Rely Guarantee for Semantic Refinement

Yannick Zakowski , David Cachera , Delphine Demange , David Pichardie
SAC 2018 - The 33rd ACM/SIGAPP Symposium On Applied Computing, Apr 2018, Pau, France. pp.1881-1890, ⟨10.1145/3167132.3167333⟩
Communication dans un congrès hal-01653620v1
Image document

Verified Translation Validation of Static Analyses

Gilles Barthe , Sandrine Blazy , Vincent Laporte , David Pichardie , Alix Trieu
Computer Security Foundations Symposium, Aug 2017, Santa-Barbara, United States
Communication dans un congrès hal-01588422v1
Image document

Verifying Constant-Time Implementations by Abstract Interpretation

Sandrine Blazy , David Pichardie , Alix Trieu
European Symposium on Research in Computer Security, Sep 2017, Oslo, Norway
Communication dans un congrès hal-01588444v1
Image document

Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology

Yannick Zakowski , David Cachera , Delphine Demange , Gustavo Petri , David Pichardie
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⟩
Communication dans un congrès hal-01613389v1
Image document

An Extended Buffered Memory Model With Full Reorderings

Gurvan Cabon , David Cachera , David Pichardie
FtFjp - Ecoop workshop, Jul 2016, Rome, Italy. pp.1 - 6, ⟨10.1145/2955811.2955816⟩
Communication dans un congrès hal-01379514v1
Image document

An Abstract Memory Functor for Verified C Static Analyzers

Sandrine Blazy , Vincent Laporte , David Pichardie
ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. pp.14, ⟨10.1145/2951913.2951937⟩
Communication dans un congrès hal-01339969v1

Verified Validation of Program Slicing

Sandrine Blazy , Andre Maroneze , David Pichardie
CPP 2015 : Conference on Certified Programs and Proofs, 2015, Mumbai, India. pp.109-117, ⟨10.1145/2676724.2693169⟩
Communication dans un congrès hal-01110821v1

Verifying Fast and Sparse SSA-based Optimizations in Coq.

Delphine Demange , David Pichardie , Léo Stefanesco
24th International Conference on Compiler Construction, CC 2015, 2015, London, United Kingdom
Communication dans un congrès hal-01110779v1
Image document

A formally-verified C static analyzer

Jacques-Henri Jourdan , Vincent Laporte , Sandrine Blazy , Xavier Leroy , David Pichardie
POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩
Communication dans un congrès hal-01078386v1
Image document

Validating Dominator Trees for a Fast, Verified Dominance Test

Sandrine Blazy , Delphine Demange , David Pichardie
Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_6⟩
Communication dans un congrès hal-01193281v1
Image document

Kharon : Découvrir, comprendre et reconnaître des malware Android par suivi de flux d'information

Radoniaina Andriatsimandefitra Ratsisahanana , Thomas Genet , Laurent Guillo , Jean-François Lalande , David Pichardie
Rendez-vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information, May 2015, Troyes, France
Communication dans un congrès hal-01154368v1
Image document

System-level Non-interference for Constant-time Cryptography

Gilles Barthe , Gustavo Betarte , Juan Diego Campo , Carlos Luna , David Pichardie
ACM SIGSAC Conference on Computer and Communications Security, CCS'14, Nov 2014, Scottsdale, United States. pp.1267 - 1279, ⟨10.1145/2660267.2660283⟩
Communication dans un congrès hal-01101950v1
Image document

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code

Sandrine Blazy , Vincent Laporte , David Pichardie
The 5th International Conference on Interactive Theorem Proving (ITP 2014), 2014, Vienna, Austria. pp.128 - 143, ⟨10.1007/978-3-319-08970-6_9⟩
Communication dans un congrès hal-01102445v1

A Formally Verified WCET Estimation Tool

André Oliveira Maroneze , Sandrine Blazy , David Pichardie , Isabelle Puaut
14th International Workshop on Worst-Case Execution Time Analysis, Jul 2014, Madrid, Spain. ⟨10.4230/OASIcs.WCET.2014.11⟩
Communication dans un congrès hal-01087194v1

A Verified Information-Flow Architecture

Arthur Azevedo de Amorim , Nathan Collins , André Dehon , Delphine Demange , Catalin Hritcu
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. ⟨10.1145/2535838.2535839⟩
Communication dans un congrès hal-00918847v1

Plan B: A Buffered Memory Model for Java

Delphine Demange , Vincent Laporte , Lei Zhao , David Pichardie , Suresh Jagannathan
Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Jan 2013, Rome, Italy
Communication dans un congrès hal-00924716v1
Image document

Formal Verification of Loop Bound Estimation for WCET Analysis

Sandrine Blazy , André Maroneze , David Pichardie
VSTTE - Verified Software: Theories, Tools and Experiments, Natarajan Shankar, May 2013, Menlo Park, United States. pp.281-303
Communication dans un congrès hal-00848703v1
Image document

Formal Verification of a C Value Analysis Based on Abstract Interpretation

Sandrine Blazy , Vincent Laporte , André Maroneze , David Pichardie
SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344
Communication dans un congrès hal-00812515v1

A Formally Verified SSA-based Middle-end

Gilles Barthe , Delphine Demange , David Pichardie
21th European Symposium on Programming, ESOP 2012, Mar 2012, Tallin, Estonia. pp.47-66, ⟨10.1007/978-3-642-28869-2_3⟩
Communication dans un congrès hal-01110783v1
Image document

Modular SMT Proofs for Fast Reflexive Checking inside Coq

Frédéric Besson , Pierre-Emmanuel Cornilleau , David Pichardie
First International Conference on Certified Programs and Proofs, 2011, Kenting, Taiwan
Communication dans un congrès hal-00646960v1
Image document

Secure the Clones - Static Enforcement of Policies for Secure Object Copying

Thomas Jensen , Florent Kirchner , David Pichardie
ESOP 2011, 2011, Saarbrucken, Germany
Communication dans un congrès hal-01110817v1
Image document

A Nelson-Oppen based Proof System using Theory Specific Proof Systems

Frédéric Besson , Pierre-Emmanuel Cornilleau , David Pichardie
First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland
Communication dans un congrès hal-00677193v1
Image document

Enforcing Secure Object Initialization in Java

Laurent Hubert , Thomas Jensen , Vincent Monfort , David Pichardie
15th European Symposium on Research in Computer Security (ESORICS), 2010, Athènes, Greece. pp.101-115
Communication dans un congrès inria-00503953v1
Image document

Sawja: Static Analysis Workshop for Java

Laurent Hubert , Nicolas Barré , Frédéric Besson , Delphine Demange , Thomas Jensen
The International Conference on Formal Verification of Object-Oriented Software, Beckert, Bernhard and Marché, Claude, 2010, Paris, France. pp.253--267
Communication dans un congrès inria-00504047v1
Image document

Certified Result Checking for Polyhedral Analysis of Bytecode Programs

Frédéric Besson , Thomas Jensen , David Pichardie , Tiphaine Turpin
The 5th International Symposium on Trustworthy Global Computing (TGC), 2010, Munich, Germany
Communication dans un congrès inria-00537816v1
Image document

A Certified Denotational Abstract Interpreter

David Cachera , David Pichardie
International Conference on Interactive Theorem Proving (ITP), 2010, Edimburgh, United Kingdom. pp.9-24
Communication dans un congrès inria-00537810v1
Image document

A Provably Correct Stackless Intermediate Representation for Java Bytecode

Delphine Demange , Thomas Jensen , David Pichardie
The 8th Asian Symposium on Programming Languages and Systems (APLAS), 2010, Shangai, China
Communication dans un congrès inria-00537815v1
Image document

Sécurité de la plate-forme d'exécution Java : limites et propositions d'améliorations

Guillaume Hiet , Frédéric Guihéry , Goulven Guiheux , David Pichardie , Christian Brunette
Symposium sur la sécurité des technologies de l'information et des communications (SSTIC), 2010, Rennes, France
Communication dans un congrès inria-00537820v1
Image document

Comparing Techniques for Certified Static Analysis

David Cachera , David Pichardie
The NASA Formal Methods Symposium (NFM), 2009, Moffett Field, United States. pp.111-115
Communication dans un congrès inria-00538772v1
Image document

Certified Static Analysis by Abstract Interpretation

Frédéric Besson , David Cachera , Thomas Jensen , David Pichardie
Foundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. pp.223-257
Communication dans un congrès inria-00538753v1

A Certified Data Race Analysis for a Java-like Language

Frédéric Dabrowski , David Pichardie
TPHOL'09, 2009, Germany. pp.212--227
Communication dans un congrès hal-00465547v1
Image document

Building certified static analysers by modular construction of well-founded lattices

David Pichardie
Proc. of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS'08), 2008, Shangai, China
Communication dans un congrès inria-00332365v1
Image document

Semantic Foundations and Inference of Non-null Annotations

Laurent Hubert , Thomas Jensen , David Pichardie
10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), 2008, Oslo, Norway
Communication dans un congrès inria-00332356v1
Image document

Preservation of proof obligations for hybrid verification methods

Gilles Barthe , César Kunz , David Pichardie , Julian Samborski-Forlese
6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08), 2008, Cape Town, South Africa
Communication dans un congrès inria-00332718v1
Image document

Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant

Gilles Barthe , Julien Forest , David Pichardie , Vlad Rusu
Functional and Logic Programming (FLOPS'06), 2006, Fuji Susono, Japan
Communication dans un congrès inria-00564237v1
Image document

Extracting a Data Flow Analyser in Constructive Logic

David Cachera , Thomas Jensen , David Pichardie , Vlad Rusu
ESOP, 2004, Barcelona, Spain
Communication dans un congrès inria-00564633v1
Image document

Formalizing Convex Hulls Algorithms

David Pichardie , Yves Bertot
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⟩
Communication dans un congrès hal-01702679v1

Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings

Sandrine Blazy , Christine Paulin-Mohring , David Pichardie
Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David. Springer, 7998, pp.500, 2013, Lecture Notes in Computer Science, ⟨10.1007/978-3-642-39634-2⟩
Ouvrages hal-00908865v1
Image document

Flow insensitive relational static analysis

Solène Mirliaz , David Pichardie
[Internship report] ENS Rennes; Université Rennes 1. 2019
Rapport hal-02332139v1
Image document

Compilation of Linearizable Data Structures

Yannick Zakowski , David Cachera , Delphine Demange , David Pichardie
[Research Report] ENS Rennes; IRISA, Inria Rennes; Université Rennes 1. 2017
Rapport hal-01538128v1
Image document

Formal Verification of an SSA-based Middle-end for CompCert

Gilles Barthe , Delphine Demange , David Pichardie
[University works] 2011
Rapport inria-00634702v3
Image document

A Provably Correct Stackless Intermediate Representation For Java Bytecode

Delphine Demange , Thomas Jensen , David Pichardie
[Research Report] RR-7021, INRIA. 2010, pp.59
Rapport inria-00414099v3
Image document

Semantic foundations and inference of non-null annotations

Laurent Hubert , Thomas Jensen , David Pichardie
[Research Report] RR-6482, INRIA. 2008
Rapport inria-00266171v2
Image document

Result certification for relational program analysis

Frédéric Besson , Thomas Jensen , David Pichardie , Tiphaine Turpin
[Research Report] RR-6333, INRIA. 2007, pp.32
Rapport inria-00166930v4
Image document

A PCC Architecture based on Certified Abstract Interpretation

Frédéric Besson , Thomas Jensen , David Pichardie
[Research Report] RR-5751, INRIA. 2005, pp.35
Rapport inria-00070268v1
Image document

Defining and Reasoning About General Recursive Functions in Type Theory: a Practical Method

David Pichardie , Vlad Rusu
[Research Report] PI 1766, 2005, pp.16
Rapport inria-00000910v1
Image document

A PCC Architecture based on Certified Abstract Interpretation

Frédéric Besson , Thomas Jensen , David Pichardie
[Research Report] PI 1764, 2005, pp.35
Rapport inria-00000866v1