Gerwin Klein

Cited by

	All	Since 2017
Citations	7039	3190
h-index	31	20
i10-index	73	47

600

300

150

450

20022003200420052006200720082009201020112012201320142015201620172018201920202021202219 53 39 64 65 113 172 243 335 283 349 413 471 512 590 584 567 559 512 497 464

Public access

View all

28 articles

0 articles

available

not available

Based on funding mandates

Co-authors

June AndronickPrincipal Research Scientist, Data61, CSIROVerified email at data61.csiro.au
Gernot HeiserProfessor of Computer Science, UNSW SydneyVerified 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 NorrishAustralian National UniversityVerified email at anu.edu.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
Liam O'ConnorUniversity of EdinburghVerified email at ed.ac.uk
Gabriele KellerUtrecht UniversityVerified email at uu.nl
Dhammika ElkaduweUniversity of Peradeniya (www.pdn.ac.lk)Verified email at ce.pdn.ac.lk
Christine RizkallahSenior Lecturer at the University of MelbourneVerified email at unimelb.edu.au
Peter GammieANUVerified email at anu.edu.au
Daniel MatichukPhD Graduate, UNSWVerified email at unswalumni.com
Matthew FernandezIntel LabsVerified email at intel.com
Mark StaplesData61, CSIROVerified email at data61.csiro.au
Yutaka NagashimaHuawei Technologies R&D (UK)Verified email at huawei.com
David GreenawayNICTA and School of Computer Science, University of New South WalesVerified email at cse.unsw.edu.au
Timothy BourkeVerified email at tbrk.org
Lawrence PaulsonUniversity of CambridgeVerified email at cam.ac.uk

Gerwin Klein

Proofcraft and UNSW

Verified email at 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	2513*	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	406	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	357	2006
Concrete semantics: with Isabelle/HOL T Nipkow, G Klein Springer International Publishing, 2014	256	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	255	2013
Types, bytes, and separation logic H Tuch, G Klein, M Norrish Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2007	231	2007
Operating system verification—an overview G Klein Sadhana 34 (1), 27-69, 2009	188	2009
Translation validation for a verified OS kernel TAL Sewell, MO Myreen, G Klein Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013	170	2013
JFlex-The Fast Scanner Generator for Java G Klein, S Rowe, R Décamps URL: http://www. jflex. de, 2005	143*	2005
Verified bytecode verifiers G Klein, T Nipkow Theoretical Computer Science 298 (3), 583-626, 2003	139	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	133	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	114	2016
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	109	2008
seL4 enforces integrity T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein International Conference on Interactive Theorem Proving, 325-340, 2011	108	2011
Verified protection model of the seL4 microkernel D Elkaduwe, G Klein, K Elphinstone Working Conference on Verified Software: Theories, Tools, and Experiments …, 2008	81	2008
Bridging the gap: Automatic verified abstraction of C D Greenaway, J Andronick, G Klein International Conference on Interactive Theorem Proving, 99-115, 2012	76	2012
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	71	2014
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	71	2012
Verified lightweight bytecode verification G Klein, T Nipkow Concurrency and Computation: Practice and Experience 13 (13), 1133-1151, 2001	71	2001
Towards a Practical, Verified Kernel. K Elphinstone, G Klein, P Derrin, T Roscoe, G Heiser HotOS, 2007	67	2007

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

Follow

Cited by

Co-authors