| seL4: Formal Verification of an Operating-System Kernel SW Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David ... Communications of the ACM 53 (6), 107-115, 2010 | 2924* | 2010 |
| Comprehensive formal verification of an OS microkernel G Klein, J Andronick, K Elphinstone, T Murray, T Sewell, R Kolanski, ... ACM Transactions on Computer Systems (TOCS) 32 (1), 1-70, 2014 | 531 | 2014 |
| A machine-checked model for a Java-like language, virtual machine, and compiler G Klein, T Nipkow ACM Transactions on Programming Languages and Systems (TOPLAS) 28 (4), 619-695, 2006 | 374 | 2006 |
| seL4: from general purpose to a proof of information flow enforcement T Murray, D Matichuk, M Brassil, P Gammie, T Bourke, S Seefried, ... 2013 IEEE Symposium on Security and Privacy, 415-429, 2013 | 308 | 2013 |
| Concrete semantics: with Isabelle/HOL T Nipkow, G Klein Springer International Publishing, 2014 | 306 | 2014 |
| Types, bytes, and separation logic H Tuch, G Klein, M Norrish Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2007 | 250 | 2007 |
| Translation validation for a verified OS kernel TAL Sewell, MO Myreen, G Klein Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013 | 227 | 2013 |
| Operating system verification—an overview G Klein Sadhana 34 (1), 27-69, 2009 | 197 | 2009 |
| JFlex-The Fast Scanner Generator for Java G Klein, S Rowe, R Décamps URL: http://www. jflex. de, 2005 | 152* | 2005 |
| Verified bytecode verifiers G Klein, T Nipkow Theoretical Computer Science 298 (3), 583-626, 2003 | 141 | 2003 |
| Towards trustworthy computing systems: taking microkernels to the next level G Heiser, K Elphinstone, I Kuz, G Klein, SM Petters ACM SIGOPS Operating Systems Review 41 (4), 3-11, 2007 | 140 | 2007 |
| Cogent: Verifying high-assurance file system implementations S Amani, A Hixon, Z Chen, C Rizkallah, P Chubb, L O'Connor, J Beeren, ... ACM SIGARCH Computer Architecture News 44 (2), 175-188, 2016 | 139 | 2016 |
| seL4 enforces integrity T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein International Conference on Interactive Theorem Proving, 325-340, 2011 | 124 | 2011 |
| Secure microkernels, state monads and scalable refinement D Cock, G Klein, T Sewell Theorem Proving in Higher Order Logics: 21st International Conference …, 2008 | 117 | 2008 |
| Don't sweat the small stuff: formal verification of C code without the pain D Greenaway, J Lim, J Andronick, G Klein ACM SIGPLAN Notices 49 (6), 429-439, 2014 | 90 | 2014 |
| Bridging the gap: Automatic verified abstraction of C D Greenaway, J Andronick, G Klein Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012 | 89 | 2012 |
| Noninterference for operating system kernels T Murray, D Matichuk, M Brassil, P Gammie, G Klein Certified Programs and Proofs: Second International Conference, CPP 2012 …, 2012 | 87 | 2012 |
| Verified protection model of the seL4 microkernel D Elkaduwe, G Klein, K Elphinstone Verified Software: Theories, Tools, Experiments: Second International …, 2008 | 87 | 2008 |
| Mind the gap: A verification framework for low-level C S Winwood, G Klein, T Sewell, J Andronick, D Cock, M Norrish Theorem Proving in Higher Order Logics: 22nd International Conference …, 2009 | 67 | 2009 |
| Towards a Practical, Verified Kernel. K Elphinstone, G Klein, P Derrin, T Roscoe, G Heiser HotOS, 2007 | 67 | 2007 |
June AndronickCEO and co-founcer, Proofcraft確認したメール アドレス: proofcraft.systems