| A formally-verified C static analyzer JH Jourdan, V Laporte, S Blazy, X Leroy, D Pichardie Acm Sigplan Notices 50 (1), 247-259, 2015 | 222 | 2015 |
| System-level non-interference for constant-time cryptography G Barthe, G Betarte, J Campo, C Luna, D Pichardie Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications …, 2014 | 181 | 2014 |
| A certified lightweight non-interference java bytecode verifier G Barthe, D Pichardie, T Rezk Programming Languages and Systems: 16th European Symposium on Programming …, 2007 | 121 | 2007 |
| A verified information-flow architecture A Azevedo de Amorim, N Collins, A DeHon, D Demange, C Hriţcu, ... Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of …, 2014 | 119 | 2014 |
| Formal verification of a constant-time preserving C compiler G Barthe, S Blazy, B Grégoire, R Hutin, V Laporte, D Pichardie, A Trieu Proceedings of the ACM on Programming Languages 4 (POPL), 1-30, 2019 | 115 | 2019 |
| Extracting a data flow analyser in constructive logic D Cachera, T Jensen, D Pichardie, V Rusu European Symposium on Programming, 385-400, 2004 | 106 | 2004 |
| A formally verified SSA-based middle-end: Static single assignment meets CompCert G Barthe, D Demange, D Pichardie European Symposium on Programming, 47-66, 2012 | 101* | 2012 |
| Proof-carrying code from certified abstract interpretation and fixpoint compression F Besson, T Jensen, D Pichardie Theoretical Computer Science 364 (3), 273-291, 2006 | 81 | 2006 |
| Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant G Barthe, J Forest, D Pichardie, V Rusu Functional and Logic Programming: 8th International Symposium, FLOPS 2006 …, 2006 | 79 | 2006 |
| Semantic foundations and inference of non-null annotations L Hubert, T Jensen, D Pichardie International Conference on Formal Methods for Open Object-Based Distributed …, 2008 | 71 | 2008 |
| Verifying constant-time implementations by abstract interpretation S Blazy, D Pichardie, A Trieu Journal of Computer Security 27 (1), 137-163, 2019 | 68 | 2019 |
| Certified memory usage analysis D Cachera, T Jensen, D Pichardie, G Schneider FM 2005: Formal Methods: International Symposium of Formal Methods Europe …, 2005 | 60 | 2005 |
| Formal verification of a C value analysis based on abstract interpretation S Blazy, V Laporte, A Maroneze, D Pichardie Static Analysis: 20th International Symposium, SAS 2013, Seattle, WA, USA …, 2013 | 59 | 2013 |
| Formalizing convex hull algorithms D Pichardie, Y Bertot International Conference on Theorem Proving in Higher Order Logics, 346-361, 2001 | 59* | 2001 |
| Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés D Pichardie PhD thesis, University Rennes 1, 2005 | 57 | 2005 |
| The MOBIUS Proof Carrying Code Infrastructure: (An Overview) G Barthe, P Crégut, B Grégoire, T Jensen, D Pichardie International Symposium on Formal Methods for Components and Objects, 1-24, 2007 | 46 | 2007 |
| A certified denotational abstract interpreter D Cachera, D Pichardie International Conference on Interactive Theorem Proving, 9-24, 2010 | 45 | 2010 |
| Plan B: A buffered memory model for Java D Demange, V Laporte, L Zhao, S Jagannathan, D Pichardie, J Vitek Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013 | 44 | 2013 |
| Sawja: Static analysis workshop for java L Hubert, N Barré, F Besson, D Demange, T Jensen, V Monfort, ... International Conference on Formal Verification of Object-Oriented Software …, 2010 | 44 | 2010 |
| A certified lightweight non-interference java bytecode verifier G Barthe, D Pichardie, T Rezk Mathematical Structures in Computer Science 23 (5), 1032-1081, 2013 | 39 | 2013 |
Thomas JensenDirecteur de recherche INRIA Rennes and IRISAVerified email at inria.fr
