David Pichardie

According to our database, David Pichardie authored at least 64 papers between 2001 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

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., January, 2023

Leveraging Static Analysis for Bug Repair.

Ruba Mutasim, Gabriel Synnaeve, David Pichardie, Baptiste Rozière

CoRR, 2023

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

A Flow-Insensitive-Complete Program Representation.

Solène Mirliaz, David Pichardie

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs.

Gilles Barthe, Adrien Koutsos, Solène Mirliaz, David Pichardie, Peter Schwabe

Proceedings of the Static Analysis - 29th International Symposium, 2022

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

Verified Functional Programming of an Abstract Interpreter.

Lucas Franceschino, David Pichardie, Jean-Pierre Talpin

Proceedings of the Static Analysis - 28th International Symposium, 2021

Secure Compilation of Constant-Resource Programs.

Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

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

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, David Pichardie

J. Autom. Reason., 2020

A Fast Verified Liveness Analysis in SSA Form.

Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Verifying constant-time implementations by abstract interpretation.

Sandrine Blazy, David Pichardie, Alix Trieu

J. Comput. Secur., 2019

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

2018

Preface.

David Pichardie, Mihaela Sighireanu

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2018

Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement.

Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie

Proceedings of the 33rd Annual ACM Symposium on Applied Computing, 2018

Semantic reasoning about the sea of nodes.

Delphine Demange, Yon Fernández de Retana, David Pichardie

Proceedings of the 27th International Conference on Compiler Construction, 2018

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

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Verified Translation Validation of Static Analyses.

Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu

Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

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 Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code.

Sandrine Blazy, Vincent Laporte, David Pichardie

J. Autom. Reason., 2016

An abstract memory functor for verified C static analyzers.

Sandrine Blazy, Vincent Laporte, David Pichardie

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

An Extended Buffered Memory Model With Full Reorderings.

Gurvan Cabon, David Cachera, David Pichardie

Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs, 2016

2015

A Formally-Verified C Static Analyzer.

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Validating Dominator Trees for a Fast, Verified Dominance Test.

Sandrine Blazy, Delphine Demange, David Pichardie

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Verified Validation of Program Slicing.

Sandrine Blazy, André Maroneze, David Pichardie

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

Verifying Fast and Sparse SSA-Based Optimizations in Coq.

Delphine Demange, David Pichardie, Léo Stefanesco

Proceedings of the Compiler Construction - 24th International Conference, 2015

2014

Atomicity Refinement for Verified Compilation.

Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek

ACM Trans. Program. Lang. Syst., 2014

Formal Verification of an SSA-Based Middle-End for CompCert.

Gilles Barthe, Delphine Demange, David Pichardie

ACM Trans. Program. Lang. Syst., 2014

System-level non-interference for constant-time cryptography.

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie

IACR Cryptol. ePrint Arch., 2014

A Formally Verified WCET Estimation Tool.

André Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut

Proceedings of the 14th International Workshop on Worst-Case Execution Time Analysis, 2014

2013

A certified lightweight non-interference Java bytecode verifier.

Gilles Barthe, David Pichardie, Tamara Rezk

Math. Struct. Comput. Sci., 2013

Formal Verification of Loop Bound Estimation for WCET Analysis.

Sandrine Blazy, André Maroneze, David Pichardie

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Formal Verification of a C Value Analysis Based on Abstract Interpretation.

Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie

Proceedings of the Static Analysis - 20th International Symposium, 2013

Plan B: a buffered memory model for Java.

Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, Jan Vitek

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

2012

Secure the Clones

Thomas P. Jensen, Florent Kirchner, David Pichardie

Log. Methods Comput. Sci., 2012

A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert.

Gilles Barthe, Delphine Demange, David Pichardie

Proceedings of the Programming Languages and Systems, 2012

Toward a Verified Software Toolchain for Java.

David Pichardie

, 2012

2011

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

David Cachera, David Pichardie

Tech. Sci. Informatiques, 2011

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

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

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

Thomas P. Jensen, Florent Kirchner, David Pichardie

Proceedings of the Programming Languages and Systems, 2011

Modular SMT Proofs for Fast Reflexive Checking Inside Coq.

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Verifying resource access control on mobile interactive devices.

Frédéric Besson, Guillaume Dufay, Thomas P. Jensen, David Pichardie

J. Comput. Secur., 2010

Preface.

David Pichardie

Proceedings of the Fifth Workshop on Bytecode Semantics, 2010

Certified Result Checking for Polyhedral Analysis of Bytecode Programs.

Frédéric Besson, Thomas P. Jensen, David Pichardie, Tiphaine Turpin

Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

A Certified Denotational Abstract Interpreter.

David Cachera, David Pichardie

Proceedings of the Interactive Theorem Proving, First International Conference, 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

Proceedings of the Formal Verification of Object-Oriented Software, 2010

Enforcing Secure Object Initialization in Java.

Laurent Hubert, Thomas P. Jensen, Vincent Monfort, David Pichardie

Proceedings of the Computer Security, 2010

A Provably Correct Stackless Intermediate Representation for Java Bytecode.

Delphine Demange, Thomas P. Jensen, David Pichardie

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009

Soundly Handling Static Fields: Issues, Semantics and Analysis.

Laurent Hubert, David Pichardie

Proceedings of the Fourth Workshop on Bytecode Semantics, 2009

A Certified Data Race Analysis for a Java-like Language.

Frédéric Dabrowski, David Pichardie

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Comparing Techniques for Certified Static Analysis.

David Cachera, David Pichardie

Proceedings of the First NASA Formal Methods Symposium, 2009

Certified Static Analysis by Abstract Interpretation.

Frédéric Besson, David Cachera, Thomas P. Jensen, David Pichardie

Proceedings of the Foundations of Security Analysis and Design V, 2009

2008

Building Certified Static Analysers by Modular Construction of Well-founded Lattices.

David Pichardie

Proceedings of the First International Conference on Foundations of Informatics, 2008

Preservation of Proof Pbligations for Hybrid Verification Methods.

Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese

Proceedings of the Sixth IEEE International Conference on Software Engineering and Formal Methods, 2008

Semantic Foundations and Inference of Non-null Annotations.

Laurent Hubert, Thomas P. Jensen, David Pichardie

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2008

2007

The MOBIUS Proof Carrying Code Infrastructure.

Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie

Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

2006

Proof-carrying code from certified abstract interpretation and fixpoint compression.

Frédéric Besson, Thomas P. Jensen, David Pichardie

Theor. Comput. Sci., 2006

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant.

Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu

Proceedings of the Functional and Logic Programming, 8th International Symposium, 2006

2005

Extracting a data flow analyser in constructive logic.

David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu

Theor. Comput. Sci., 2005

Certified Memory Usage Analysis.

David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider

Proceedings of the FM 2005: Formal Methods, 2005

Modular Proof Principles for Parameterised Concretizations.

David Pichardie

Proceedings of the Construction and Analysis of Safe, 2005

2003

A Java Card CAP converter in PVS.

Thomas Genet, Thomas P. Jensen, Vikash Kodati, David Pichardie

Proceedings of the Compiler Optimization Meets Compiler Verification, 2003

Embedding of Systems of Affine Recurrence Equations in Coq.

David Cachera, David Pichardie

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

2001

Formalizing Convex Hull Algorithms.

David Pichardie, Yves Bertot

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001