Follow
Gerwin Klein
Title
Cited by
Cited by
Year
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
2542*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
4182014
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
3642006
Concrete semantics: with Isabelle/HOL
T Nipkow, G Klein
Springer International Publishing, 2014
2632014
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
2632013
Types, bytes, and separation logic
H Tuch, G Klein, M Norrish
Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2007
2322007
Operating system verification—an overview
G Klein
Sadhana 34 (1), 27-69, 2009
1932009
Translation validation for a verified OS kernel
TAL Sewell, MO Myreen, G Klein
Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013
1772013
JFlex-The Fast Scanner Generator for Java
G Klein, S Rowe, R Décamps
URL: http://www. jflex. de, 2005
141*2005
Verified bytecode verifiers
G Klein, T Nipkow
Theoretical Computer Science 298 (3), 583-626, 2003
1392003
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
1322007
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
1152016
seL4 enforces integrity
T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein
Interactive Theorem Proving: Second International Conference, ITP 2011, Berg …, 2011
1102011
Secure microkernels, state monads and scalable refinement
D Cock, G Klein, T Sewell
Theorem Proving in Higher Order Logics: 21st International Conference …, 2008
1082008
Verified protection model of the seL4 microkernel
D Elkaduwe, G Klein, K Elphinstone
Verified Software: Theories, Tools, Experiments: Second International …, 2008
842008
Bridging the gap: Automatic verified abstraction of C
D Greenaway, J Andronick, G Klein
Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012
762012
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
722012
Verified lightweight bytecode verification
G Klein, T Nipkow
Concurrency and Computation: Practice and Experience 13 (13), 1133-1151, 2001
712001
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
692014
Towards a Practical, Verified Kernel.
K Elphinstone, G Klein, P Derrin, T Roscoe, G Heiser
HotOS, 2007
672007
The system can't perform the operation now. Try again later.
Articles 1–20