Gerwin Klein
Hivatkozott rá
Hivatkozott rá
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
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
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
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
Concrete semantics: with Isabelle/HOL
T Nipkow, G Klein
Springer International Publishing, 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
Translation validation for a verified OS kernel
TAL Sewell, MO Myreen, G Klein
Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013
Operating system verification—an overview
G Klein
Sadhana 34 (1), 27-69, 2009
JFlex-The Fast Scanner Generator for Java
G Klein, S Rowe, R Décamps
URL: http://www. jflex. de, 2005
Verified bytecode verifiers
G Klein, T Nipkow
Theoretical Computer Science 298 (3), 583-626, 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
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
seL4 enforces integrity
T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein
International Conference on Interactive Theorem Proving, 325-340, 2011
Secure microkernels, state monads and scalable refinement
D Cock, G Klein, T Sewell
Theorem Proving in Higher Order Logics: 21st International Conference …, 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
Verified protection model of the seL4 microkernel
D Elkaduwe, G Klein, K Elphinstone
Verified Software: Theories, Tools, Experiments: Second International …, 2008
Bridging the gap: Automatic verified abstraction of C
D Greenaway, J Andronick, G Klein
Interactive Theorem Proving: Third International Conference, ITP 2012 …, 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
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
Towards a Practical, Verified Kernel.
K Elphinstone, G Klein, P Derrin, T Roscoe, G Heiser
HotOS, 2007
A rendszer jelenleg nem tudja elvégezni a műveletet. Próbálkozzon újra később.
Cikkek 1–20