Publications of David Pichardie

Load the BibTeX file

Books

  1. Sandrine Blazy, Christine Paulin-Mohring, David Pichardie. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Sandrine Blazy, Christine Paulin-Mohring, David PichardieS. Blazy, C. Paulin-Mohring, D. Pichardie (eds.), Lecture Notes in Computer Science, Springer, 2013. download

Academic Journals

  1. Gilles Barthe, David Pichardie, Tamara Rezk. A certified lightweight non-interference Java bytecode verifier. Mathematical Structures in Computer Science, 23(5):1032-1081, June 2013. download
  2. Thomas Jensen, Florent Kirchner, David Pichardie. Secure the Clones: Static Enforcement of Policies for Secure Object Copying. Logical Methods in Computer Science (LMCS), 8(2), 2012.
  3. Frédéric Besson, Thomas Jensen, Guillaume Dufay, David Pichardie. Verifying Resource Access Control on Mobile Interactive Devices. Journal of Computer Security, 18(6):971-998, 2010.
  4. Frédéric Besson, Thomas Jensen, David Pichardie. Proof-Carrying Code from Certified Abstract Interpretation to Fixpoint Compression. Theoretical Computer Science, 364(3):273-291, 2006.
  5. David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science, 2005.

International Conferences

  1. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach. A Verified Information-Flow Architecture. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), To appear, San Diego, CA, United States, 2014. download
  2. Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. In SAS - 20th Static Analysis Symposium, Manuel Fahndrich, Francesco Logozzo (eds.), Volume Lecture Notes in Computer Science, Pages 324-344, Seattle, United States, 2013. download
  3. Sandrine Blazy, André Maroneze, David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. In VSTTE - Verified Software: Theories, Tools and Experiments, Ernie Cohen, Andrey Rybalchenko (eds.), Lecture Notes in Computer Science, Volume 8164, Pages 281-303, Menlo Park, United States, 2013. download
  4. Delphine Demange, Vincent Laporte, Lei Zhao, David Pichardie, Suresh Jagannathan, Jan Vitek. Plan B: A Buffered Memory Model for Java. In Proc. of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 2013. download
  5. Gilles Barthe, Delphine Demange, David Pichardie. A formally verified SSA-based middle-end - Static Single Assignment meets CompCert. In Proc. of 21th European Symposium on Programming (ESOP 2012), Lecture Notes in Computer Science, Volume 7211, Pages 47-66, 2012.
  6. Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. A Nelson-Oppen based Proof System using Theory Specific Proof Systems. In Workshop on Proof eXchange for Theorem Proving (PxTP), 2011.
  7. Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. Modular SMT Proofs for Fast Reflexive Checking inside Coq. In First International Conference on Certified Programs and Proofs, Lecture Notes in Computer Science, Volume 7086, Pages 151-166, Kenting, Taiwan, Province De Chine, 2011. download
  8. Thomas Jensen, Florent Kirchner, David Pichardie. Secure the Clones: Static Enforcement of Policies for Secure Object Copying. In Proc. of 20th European Symposium on Programming (ESOP 2011), Lecture Notes in Computer Science, Volume 6602, Pages 317-337, 2011.
  9. Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation for Java Bytecode. In 8th Asian Symposium on Programming Languages and Systems (APLAS), Lecture Notes in Computer Science, Volume 6461, 2010.
  10. David Cachera, David Pichardie. A Certified Denotational Abstract Interpreter. In Proc.\ of International Conference on Interactive Theorem Proving (ITP-10), Lecture Notes in Computer Science, Volume 6172, Pages 9-24, 2010.
  11. Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin. Certified Result Checking for Polyhedral Analysis of Bytecode Programs. In Proc.\ of the 5th International Symposium on Trustworthy Global Computing (TGC 2010), Lecture Notes in Computer Science, Volume 6084, Pages 253-267, 2010.
  12. Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie, Tiphaine Turpin. Sawja: Static Analysis Workshop for Java. In 1st International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Lecture Notes in Computer Science, 2010.
  13. Laurent Hubert, Thomas Jensen, Vincent Monfort, David Pichardie. Enforcing Secure Object Initialization in Java. In 15th European Symposium on Research in Computer Security (ESORICS), Lecture Notes in Computer Science, Volume 6345, Pages 101-115, 2010.
  14. Frédéric Dabrowski, David Pichardie. A Certified Data Race Analysis for a Java-like Language. In Proc.\ of 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), Lecture Notes in Computer Science, Volume 5674, Pages 212-227, 2009.
  15. David Cachera, David Pichardie. Comparing Techniques for Certified Static Analysis. In Proc.\ of the 1st NASA Formal Methods Symposium (NFM'09), Pages 111-115, 2009.
  16. Laurent Hubert, David Pichardie. Soundly Handling Static Fields: Issues, Semantics and Analysis. In Proc.\ of the 4th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09), Electronic Notes in Theoretical Computer Science, Volume 253, Pages 15-30, 2009.
  17. Laurent Hubert, Thomas Jensen, David Pichardie. Semantic foundations and inference of non-null annotations. In Proc.\ of the 10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), Lecture Notes in Computer Science, Volume 5051, Pages 132-149, 2008.
  18. David Pichardie. Building certified static analysers by modular construction of well-founded lattices. In Proc. of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS'08), Electronic Notes in Theoretical Computer Science, Volume 212, Pages 225-239, 2008.
  19. Gilles Barthe, César Kunz, David Pichardie, Juli\'an Samborski Forlese. Preservation of Proof Obligations for Hybrid Certificates. In Proc.\ of the 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08), Pages 127-136, 2008.
  20. Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas Jensen, David Pichardie. The MOBIUS Proof Carrying Code infrastructure. In Proc.\ of the 6th International Symposium on Formal Methods for Components and Objects (FMCO'07), Lecture Notes in Computer Science, Volume 5382, Pages 1-24, 2008.
  21. G. Barthe, D. Pichardie, T. Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier. In Proc.\ of 16th European Symposium on Programming (ESOP'07), Lecture Notes in Computer Science, Volume 4421, Pages 125-140, 2007.
  22. Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu. Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. In Proc\. of 8th International Symposium on Functional and Logic Programming (FLOPS'06), Lecture Notes in Computer Science, Volume 3945, Pages 114-129, 2006.
  23. F. Besson, T. Jensen, D. Pichardie. A PCC Architecture based on Certified Abstract Interpretation. In Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), ENTCS, 2006. download
  24. David Pichardie. Modular proof principles for parameterized concretizations. In Proc.\ of 2nd International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS 2005), Lecture Notes in Computer Science, Pages 138-154, 2005.
  25. David Cachera, Thomas Jensen, David Pichardie, Gerardo Schneider. Certified Memory Usage Analysis. In Proc\. of 13th International Symposium on Formal Methods (FM'05), Lecture Notes in Computer Science, 2005.
  26. David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a data flow analyser in constructive logic. In Proc. ESOP'04, Springer LNCS, Pages 385-400, 2004.
  27. T. Genet, T. Jensen, V. Kodati, D. Pichardie. A Java Card CAP Converter in PVS. In Proceedings of the 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003), 2003. download
  28. David Cachera, David Pichardie. Embedding of Systems of Affine Recurrence Equations in Coq. In Proc. TPHOLs 2003, 16th International Conference on Theorem Proving in Higher Order Logics , LNCS, Rome, Italy, September 2003. ps
  29. David Pichardie, Yves Bertot. Formalizing Convex Hulls Algorithms. In Proc.\ of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), Lecture Notes in Computer Science, Pages 346-361, 2001.

National Conferences

  1. 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. In Proc.\ of Symposium sur la sécurité des technologies de l'information et des communications (SSTIC 2010), 2010.

Research Reports

  1. Gilles Barthe, Delphine Demange, David Pichardie. A formally verified SSA-based middle-end compiler. Research Report INRIA, October 2011. download
  2. Delphine Demange, Thomas Jensen, David Pichardie. A Provably Correct Stackless Intermediate Representation For Java Bytecode. Research Report INRIA, No 0, 2009. download
  3. F. Besson, T. Jensen, D. Pichardie, T. Turpin. Result certification for relational program analysis. Research Report Inria, No 6333, September 2007. download
  4. F. Besson, T. Jensen, D. Pichardie. A PCC Architecture based on Certified Abstract Interpretation. Research Report INRIA, No 0, November 2005.
  5. David Cachera, David Pichardie. Proof Tactics for the Verification of Structured Systems of Affine Recurrence Equations. Research Report INRIA, No 1511, 2003. ps

Misc

  1. Fré Besson, David Cachera, Thomas Jensen, David Pichardie. Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. pp. 223-257, 2009.
  2. David Pichardie. Les codes porteurs de preuve. pp. 8-9, 2008.

Thesis

  1. David Pichardie. Toward a Verified Software Toolchain for Java. Habilitation à diriger des recherches ENS Cachan, 2012.
  2. David Pichardie. Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certiés. PhD Thesis Université Rennes 1, Rennes, France, December 2005.