Nombre de documents

53


Article dans une revue10 documents

  • 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>
  • 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 (JCS); Special Issue on Verified Information Flow Security, 2016, 24 (6), pp.689--734. <10.3233/JCS-15784>. <hal-01424797>
  • 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 Dufay, 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. <http://www.sciencedirect.com/science/article/B75H1-4XT3BCD-3/2/0c24aba371ae79c050511b1705928a1b>. <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>

Communication dans un congrès32 documents

  • 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. ACM, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), pp.14, 2016, <http://conf.researchr.org/home/icfp-2016/>. <10.1145/2951913.2951937>. <hal-01339969>
  • Gurvan Cabon, David Cachera, David Pichardie. An Extended Buffered Memory Model With Full Reorderings. FtFjp - Ecoop workshop, Jul 2016, Rome, Italy. pp.1 - 6, 2016, <10.1145/2955811.2955816>. <hal-01379514>
  • Sandrine Blazy, Delphine Demange, David Pichardie. Validating Dominator Trees for a Fast, Verified Dominance Test. Springer. Interactive Theorem Proving, Aug 2015, Nanjing, China. Lecture Notes in Computer Science (LNCS) (9236), 2015, <10.1007/978-3-319-22102-1_6>. <hal-01193281>
  • 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>
  • 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. 2015. <hal-01110779>
  • 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. ACM, pp.247-259, <10.1145/2676726.2676966>. <hal-01078386>
  • 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>
  • 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. 2014, <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. 2014, <http://www.uni-ulm.de/en/in/wcet2014.html>. <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. Springer, 8558, pp.128 - 143, 2014, LNCS : Interactive Theorem Proving. <10.1007/978-3-319-08970-6_9>. <hal-01102445>
  • 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. ACM, pp.1267 - 1279, 2014, <http://www.sigsac.org/ccs/CCS2014/>. <10.1145/2660267.2660283>. <hal-01101950>
  • 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. ACM, 2013. <hal-00924716>
  • Sandrine Blazy, André Maroneze, David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. Ernie Cohen and Andrey Rybalchenko. VSTTE - Verified Software: Theories, Tools and Experiments, May 2013, Menlo Park, United States. Springer, 8164, pp.281-303, 2013, Lecture Notes in Computer Science. <hal-00848703>
  • Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. Manuel Fahndrich and Francesco Logozzo. SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. Springer, Lecture Notes in Computer Science, pp.324-344, 2013, 7935. <hal-00812515>
  • 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. Springer, 7211, pp.47-66, 2012, LNCS Programming Languages and Systems. <10.1007/978-3-642-28869-2_3>. <hal-01110783>
  • 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, Pierre-Emmanuel Cornilleau, David Pichardie. A Nelson-Oppen based Proof System using Theory Specific Proof Systems. Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011. <hal-00677193>
  • 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. 2011. <hal-00646960>
  • David Cachera, David Pichardie. A Certified Denotational Abstract Interpreter. International Conference on Interactive Theorem Proving (ITP), 2010, Edimburgh, United Kingdom. Springer-Verlag, 6172, pp.9-24, 2010, Lecture Notes in Computer Science. <inria-00537810>
  • 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. Springer-Verlag, 2010, Lecture Notes in Computer Science. <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. 2010. <inria-00537820>
  • Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, et al.. Sawja: Static Analysis Workshop for Java. Beckert, Bernhard and Marché, Claude. The International Conference on Formal Verification of Object-Oriented Software, 2010, Paris, France. Springer-Verlag, 2010.13, pp.253--267, 2010, Lecture Notes in Computer Science; Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France. <http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083>. <inria-00504047>
  • 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. Springer-Verlag, 6345, pp.101-115, 2010, Lecture Notes in Computer Science; Proceedings of ESORICS 2010. <inria-00503953>
  • 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. Springer-Verlag, 2010, Lecture Notes in Computer Science. <inria-00537815>
  • Frédéric Dabrowski, David Pichardie. A Certified Data Race Analysis for a Java-like Language. TPHOL'09, 2009, Germany. pp.212--227, 2009. <hal-00465547>
  • David Cachera, David Pichardie. Comparing Techniques for Certified Static Analysis. The NASA Formal Methods Symposium (NFM), 2009, Moffett Field, United States. NASA Ames Research Center, pp.111-115, 2009. <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. Springer-Verlag, 5705, pp.223-257, 2009, Lecture Notes in Computer Science; FOSAD 2007/2008/2009 Tutorial Lectures. <inria-00538753>
  • 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. 2008. <inria-00332718>
  • 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. 2008. <inria-00332356>
  • 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. 2008. <inria-00332365>
  • 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. 2006. <inria-00564237>
  • David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. ESOP, 2004, Barcelona, Spain. 2004. <inria-00564633>

Ouvrage (y compris édition critique et traduction)1 document

  • 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. Springer, 7998, pp.500, 2013, Lecture Notes in Computer Science, <10.1007/978-3-642-39634-2>. <hal-00908865>

Autre publication1 document

  • Gilles Barthe, David Pichardie, Tamara Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier. submitted to TOPLAS in September 2007. 2007. <inria-00106182v2>

Rapport8 documents

  • 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>
  • 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>
  • 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] RR-5751, INRIA. 2005, pp.35. <inria-00070268>

HDR1 document

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