Gerwin Klein

Cited by

	All	Since 2015
Citations	5771	3123
h-index	28	21
i10-index	63	41

560

280

140

420

200220032004200520062007200820092010201120122013201420152016201720182019202019 56 38 66 68 112 167 247 330 278 353 409 432 498 557 559 543 521 445

Co-authors

June AndronickPrincipal Research Scientist, Data61, CSIROVerified email at data61.csiro.au
Gernot HeiserProfessor of Computer Science, UNSW Sydney, and Data61, CSIROVerified email at unsw.edu.au
Toby MurraySchool of Computing and Information Systems, University of MelbourneVerified email at unimelb.edu.au
Kevin ElphinstoneUniversity of New South WalesVerified email at cse.unsw.edu.au
Tobias NipkowProfessor of Computer Science, Technische Universität MünchenVerified email at in.tum.de
Michael NorrishPrincipal Research Scientist, Data61Verified email at data61.csiro.au
David CockGraduate Researcher, NICTA and University of New South WalesVerified email at cse.unsw.edu.au
Ihor KuzPrincipal Research Engineer, Data61 CSIROVerified email at data61.csiro.au
Dhammika ElkaduweUniversity of Peradeniya (www.pdn.ac.lk)Verified email at ce.pdn.ac.lk
Peter GammieANUVerified email at anu.edu.au
Gabriele KellerUtrecht UniversityVerified email at uu.nl
Daniel MatichukPhD Graduate, UNSWVerified email at unswalumni.com
Kai Engelhardtghost locomotiveVerified email at gh.st
Christine RizkallahAssistant Professor (Lecturer) at the University of New South WalesVerified email at unsw.edu.au
Matthew FernandezIntel LabsVerified email at intel.com
Mark StaplesData61, CSIROVerified email at data61.csiro.au
Yutaka NagashimaCIIRC, Czech Technical University, University of InnsbruckVerified email at cvut.cz
David GreenawayNICTA and School of Computer Science, University of New South WalesVerified email at cse.unsw.edu.au
Timothy BourkeVerified email at tbrk.org
Ralf HuuckNICTA, UNSWVerified email at cse.unsw.edu.au

Gerwin Klein

Data61 and UNSW

Verified email at cse.unsw.edu.au - Homepage

formal methods interactive theorem proving software verification semantics of programming languages Isabelle/HOL


Title Sort by citations Sort by year Sort by 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	2039*	2010
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	338	2006
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	314	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	215	2007
Concrete semantics: with Isabelle/HOL T Nipkow, G Klein Springer, 2014	213	2014
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	204	2013
Operating system verification—an overview G Klein Sadhana 34 (1), 27-69, 2009	153	2009
Verified bytecode verifiers G Klein, T Nipkow Theoretical Computer Science 298 (3), 583-626, 2003	133	2003
JFlex-The Fast Scanner Generator for Java G Klein, S Rowe, R Décamps URL: http://www. jflex. de, 2005	132*	2005
Translation validation for a verified OS kernel TAL Sewell, MO Myreen, G Klein Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013	123	2013
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	114	2007
seL4 enforces integrity T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein International Conference on Interactive Theorem Proving, 325-340, 2011	90	2011
Secure microkernels, state monads and scalable refinement D Cock, G Klein, T Sewell International Conference on Theorem Proving in Higher Order Logics, 167-182, 2008	89	2008
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	78	2016
Verified lightweight bytecode verification G Klein, T Nipkow Concurrency and Computation: Practice and Experience 13 (13), 1133-1151, 2001	71	2001
Verified protection model of the seL4 microkernel D Elkaduwe, G Klein, K Elphinstone Working Conference on Verified Software: Theories, Tools, and Experiments …, 2008	70	2008
Bridging the gap: Automatic verified abstraction of C D Greenaway, J Andronick, G Klein International Conference on Interactive Theorem Proving, 99-115, 2012	63	2012
Towards a Practical, Verified Kernel. K Elphinstone, G Klein, P Derrin, T Roscoe, G Heiser HotOS, 2007	61	2007
OS Verification-Now! H Tuch, G Klein, G Heiser HotOS, 2005	60	2005
Noninterference for operating system kernels T Murray, D Matichuk, M Brassil, P Gammie, G Klein International Conference on Certified Programs and Proofs, 126-142, 2012	59	2012

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Upload PDF

Follow this author

Cited by

Co-authors