| [1] | Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, and Alix Trieu. Verified translation validation of static analyses. In IEEE 30th Computer Security Foundations Symposium, CSF 2017. IEEE Computer Society, 2017. [ bib ] |
| [2] | Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, and Jan Vitek. Verifying a concurrent garbage collector using a rely-guarantee methodology. In Proc. of the 8th International Conference on Interactive Theorem Proving (ITP 2017), volume 10499 of Lecture Notes in Computer Science. Springer-Verlag, 2017. [ bib ] |
| [3] | Sandrine Blazy, David Pichardie, and Alix Trieu. Verifying constant-time implementations by abstract interpretation. In Proc. of the 22nd European Symposium on Research in Computer Security (ESORICS 2017), volume 10492 of Lecture Notes in Computer Science. Springer-Verlag, 2017. [ bib ] |
| [4] | Sandrine Blazy, Vincent Laporte, and David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. Journal of Automated Reasoning, 56(3):26, 2016. [ bib | http ] |
| [5] | Sandrine Blazy, Vincent Laporte, and David Pichardie. An Abstract Memory Functor for Verified C Static Analyzers. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), page 14, Nara, Japan, September 2016. ACM. [ bib | http ] |
| [6] | Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. A verified information-flow architecture. Journal of Computer Security, 24(6):689--734, 2016. [ bib | http ] |
| [7] | Sandrine Blazy, Delphine Demange, and David Pichardie. Validating dominator trees for a fast, verified dominance test. In Proc. of the 6th International Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science. Springer, 2015. [ bib | .pdf | Abstract ] |
| [8] | Delphine Demange David Pichardie and Léo Stefanesco. Verifying fast and sparse ssa-based optimizations in coq. In Proc. of the 24th International Conference on Compiler Construction (CC 2015), Lecture Notes in Computer Science. Springer, 2015. [ bib | .pdf | Abstract ] |
| [9] | Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A formally-verified C static analyzer. In 42nd symposium Principles of Programming Languages, pages 247--259. ACM Press, 2015. [ bib | .pdf | Abstract ] |
| [10] | Sandrine Blazy, André Maroneze, and David Pichardie. Verified validation of program slicing. In Proc. of the 5th Conference on Certified Programs and Proofs, CPP 2015. ACM, 2015. [ bib | .pdf | Abstract ] |
| [11] | Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, and David Pichardie. System-level non-interference for constant-time cryptography. In ACM SIGSAC Conference on Computer and Communications Security, CCS'14. ACM, 2014. [ bib | .pdf | Abstract ] |
| [12] | Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, and Jan Vitek. Atomicity refinement for verified compilation. ACM Trans. Program. Lang. Syst. (TOPLAS), 36(2):1, 2014. [ bib | .pdf | Abstract ] |
| [13] | Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, and Jan Vitek. Atomicity refinement for verified compilation. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'14, page 5. ACM, 2014. Submitted and accepted to TOPLAS vol 36, presented at PLDI the same year. [ bib | .pdf | Abstract ] |
| [14] | Gilles Barthe, Delphine Demange, and David Pichardie. Formal verification of an ssa-based middle-end for compcert. ACM Trans. Program. Lang. Syst. (TOPLAS), 36(1):4, 2014. [ bib | .pdf | Abstract ] |
| [15] | Sandrine Blazy, Vincent Laporte, and David Pichardie. Verified abstract interpretation techniques for disassembling low-level self-modifying code. In Proc. of the 5th International Conference on Interactive Theorem Proving (ITP 2014), volume 8558 of Lecture Notes in Computer Science, pages 128--143. Springer, 2014. [ bib | .pdf | Abstract ] |
| [16] | André Maroneze, Sandrine Blazy, David Pichardie, and Isabelle Puaut. A formally verified wcet estimation tool. In 14th International Workshop on Worst-Case Execution Time Analysis, WCET 2014, July 8, 2014, Ulm, Germany, volume 39, pages 11--20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. [ bib | .pdf | Abstract ] |
| [17] | Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin Pierce, Randy Pollack, and Andrew Tolmach. A verified information-flow architecture. In Proc. of the 41th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pages 165--178. ACM, 2014. [ bib | .pdf | Abstract ] |
| [18] | Sandrine Blazy, André Maroneze, and David Pichardie. Formal verification of loop bound estimation for WCET analysis. In Proc. of the 5th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2013), volume 8164 of Lecture Notes in Computer Science, pages 281--303. Springer-Verlag, 2013. [ bib | .pdf | Abstract ] |
| [19] | Sandrine Blazy, Vincent Laporte, André Maroneze, and David Pichardie. Formal verification of a C value analysis based on abstract interpretation. In Proc. of the 20th Static Analysis Symposium (SAS 2013), volume 7935 of Lecture Notes in Computer Science, pages 324--344. Springer-Verlag, 2013. [ bib | .pdf | Abstract ] |
| [20] | Delphine Demange, Vincent Laporte, Lei Zhao, David Pichardie, Suresh Jagannathan, and 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. ACM, 2013. [ bib | .pdf | Abstract ] |
| [21] | Gilles Barthe, David Pichardie, and Tamara Rezk. A certified lightweight non-interference Java bytecode verifier. Mathematical Structures in Computer Science (MSCS), 23(5):1032--1081, 2013. [ bib | .pdf | Abstract ] |
| [22] | Thomas Jensen, Florent Kirchner, and David Pichardie. Secure the clones: Static enforcement of policies for secure object copying. Logical Methods in Computer Science (LMCS), 8(2), 2012. [ bib | .pdf | Abstract ] |
| [23] | Gilles Barthe, Delphine Demange, and David Pichardie. A formally verified SSA-based middle-end - Static Single Assignment meets CompCert. In Proc. of 21th European Symposium on Programming (ESOP 2012), volume 7211 of Lecture Notes in Computer Science, pages 47--66. Springer-Verlag, 2012. [ bib | .pdf | Abstract ] |
| [24] | Frédéric Besson, Pierre-Emmanuel Cornilleau, and David Pichardie. Modular SMT proofs for fast reflexive checking inside Coq. In Proc. of the 1st International Conference on Certified Programs and Proofs (CPP 2011), volume 7086 of Lecture Notes in Computer Science, pages 151--166. Springer-Verlag, 2011. [ bib | .pdf | Abstract ] |
| [25] | Thomas Jensen, Florent Kirchner, and David Pichardie. Secure the clones: Static enforcement of policies for secure object copying. In Proc. of 20th European Symposium on Programming (ESOP 2011), volume 6602 of Lecture Notes in Computer Science, pages 317--337. Springer-Verlag, 2011. [ bib | .pdf | Abstract ] |
| [26] | David Cachera and David Pichardie. Programmation d'un interpréteur abstrait certifié en logique constructive. Technique et Science Informatiques (TSI), 30(4):381--408, 2011. [ bib ] |
| [27] | David Pichardie, editor. Fifth Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2010). Proceedings, Electronic Notes in Theoretical Computer Science, 2010. [ bib ] |
| [28] | Laurent Hubert, Nicolas Barré, Frédéric Besson, Delphine Demange, Thomas Jensen, Vincent Monfort, David Pichardie, and Tiphaine Turpin. Sawja: Static Analysis Workshop for Java. In Proc. of the 1st International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), volume 6461 of Lecture Notes in Computer Science, pages 92--106. Springer-Verlag, 2010. [ bib | .pdf | Abstract ] |
| [29] | Delphine Demange, Thomas Jensen, and David Pichardie. A provably correct stackless intermediate representation for Java bytecode. In Proc. of the 8th Asian Symposium on Programming Languages and Systems (APLAS 2010), volume 6461 of Lecture Notes in Computer Science, pages 97--113. Springer-Verlag, 2010. [ bib | .pdf | Abstract ] |
| [30] | Laurent Hubert, Thomas Jensen, Vincent Monfort, and David Pichardie. Enforcing secure object initialization in Java. In Proc. of the 15th European Symposium on Research in Computer Security (ESORICS 2010), volume 6345 of Lecture Notes in Computer Science, pages 101--115. Springer-Verlag, 2010. [ bib | .pdf | Abstract ] |
| [31] | David Cachera and David Pichardie. A certified denotational abstract interpreter. In Proc. of International Conference on Interactive Theorem Proving (ITP-10), volume 6172 of Lecture Notes in Computer Science, pages 9--24. Springer-Verlag, 2010. [ bib | .pdf | Abstract ] |
| [32] | Frédéric Besson, Thomas Jensen, David Pichardie, and Tiphaine Turpin. Certified result checking for polyhedral analysis of bytecode programs. In Proc. of the 5th International Symposium on Trustworthy Global Computing (TGC 2010), volume 6084 of Lecture Notes in Computer Science, pages 253--267. Springer-Verlag, 2010. [ bib | .pdf ] |
| [33] | Guillaume Hiet, Frédéric Guihéry, Goulven Guiheux, David Pichardie, and 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. [ bib | .pdf ] |
| [34] | Frédéric Besson, Thomas Jensen, Guillaume Dufay, and David Pichardie. Verifying resource access control on mobile interactive devices. Journal of Computer Security, 18(6):971--998, 2010. [ bib | .pdf ] |
| [35] | Frédéric Besson, David Cachera, Thomas P. Jensen, and David Pichardie. Certified static analysis by abstract interpretation. In Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, volume 5705 of Lecture Notes in Computer Science, pages 223--257. Springer-Verlag, 2009. [ bib | .pdf ] |
| [36] | Frédéric Dabrowski and 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), volume 5674 of Lecture Notes in Computer Science, pages 212--227. Springer-Verlag, 2009. [ bib | .pdf ] |
| [37] | David Cachera and David Pichardie. Comparing techniques for certified static analysis. Proc. of the 1st NASA Formal Methods Symposium (NFM'09), pages 111--115, 2009. [ bib | .pdf ] |
| [38] | Laurent Hubert and David Pichardie. Soundly handling static fields: Issues, semantics and analysis. Proc. of the 4th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09), 253(5):15--30, 2009. [ bib | .pdf ] |
| [39] | Gilles Barthe, César Kunz, David Pichardie, and Julián 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. IEEE Computer Society, 2008. [ bib | .pdf ] |
| [40] | Laurent Hubert, Thomas Jensen, and 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), volume 5051 of Lecture Notes in Computer Science, pages 132--149. Springer-Verlag, 2008. [ bib | .pdf ] |
| [41] | 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), volume 212 of Electronic Notes in Theoretical Computer Science, pages 225--239, 2008. [ bib | .pdf ] |
| [42] | Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas Jensen, and David Pichardie. The MOBIUS Proof Carrying Code infrastructure. In Proc. of the 6th International Symposium on Formal Methods for Components and Objects (FMCO'07), volume 5382 of Lecture Notes in Computer Science, pages 1--24. Springer-Verlag, 2007. [ bib ] |
| [43] | Gilles Barthe, David Pichardie, and Tamara Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier. In Proc. of 16th European Symposium on Programming (ESOP'07), volume 4421 of Lecture Notes in Computer Science, pages 125--140. Springer-Verlag, 2007. [ bib | .pdf ] |
| [44] | Frédéric Besson, Thomas Jensen, and David Pichardie. Proof-carrying code from certified abstract interpretation to fixpoint compression. Theoretical Computer Science, 364(3):273--291, 2006. [ bib | .pdf ] |
| [45] | Frédéric Besson, Thomas Jensen, and David Pichardie. A PCC Architecture based on Certified Abstract Interpretation. In Proc. of 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), ENTCS. Springer-Verlag, 2006. [ bib | .pdf ] |
| [46] | Gilles Barthe, Julien Forest, David Pichardie, and 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), volume 3945 of Lecture Notes in Computer Science, pages 114--129. Springer-Verlag, 2006. [ bib | .pdf ] |
| [47] | Pichardie David. Interprétation abstraite en logique intuitionniste : extraction d'analyseurs Java certifiés. PhD thesis, Université Rennes 1, 2005. In french. [ bib | .pdf ] |
| [48] | 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), number 3956 in Lecture Notes in Computer Science, pages 138--154. Springer-Verlag, 2005. [ bib | .pdf ] |
| [49] | David Cachera, Thomas Jensen, David Pichardie, and Gerardo Schneider. Certified Memory Usage Analysis. In Proc. of 13th International Symposium on Formal Methods (FM'05), number 3582 in Lecture Notes in Computer Science, pages 91--106. Springer-Verlag, 2005. [ bib | .pdf ] |
| [50] | David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science, 342(1):56--78, September 2005. Extended version of [51]. [ bib | .pdf ] |
| [51] | David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. In Proc. of 13th European Symposium on Programming (ESOP'04), number 2986 in Lecture Notes in Computer Science, pages 385--400. Springer-Verlag, 2004. [ bib | .pdf ] |
| [52] | Thomas Genet, Thomas Jensen, Vikash Kodati, and David Pichardie. A Java Card CAP converter in PVS. In Jens Knoop and Wolf Zimmermann, editors, Proc. of 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003), ENTCS, volume 82. Elsevier, 2004. [ bib | .pdf ] |
| [53] | David Cachera and David Pichardie. Embedding of Systems of Affine Recurrence Equations in Coq. In Proc. of 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03), number 2758 in Lecture Notes in Computer Science, pages 155--170. Springer-Verlag, 2003. [ bib | .pdf ] |
| [54] | David Pichardie and Yves Bertot. Formalizing Convex Hulls Algorithms. In Proc. of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), number 2152 in Lecture Notes in Computer Science, pages 346--361. Springer-Verlag, 2001. [ bib | .pdf ] |
This file was generated by bibtex2html 1.98.