Gerwin Klein

Cited by

	All	Since 2020
Citations	8159	2572
h-index	34	21
i10-index	79	40

600

300

150

450

2003200420052006200720082009201020112012201320142015201620172018201920202021202220232024202552 44 64 69 111 181 237 334 282 350 412 477 499 591 579 560 591 500 492 523 520 494 42

Public access

View all

30 articles

0 articles

available

not available

Based on funding mandates

Co-authors

June AndronickCEO and co-founcer, ProofcraftVerified email at proofcraft.systems
Gernot HeiserProfessor of Computer Science, University of New South WalesVerified 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 CockSenior Researcher, ETH ZurichVerified email at cse.unsw.edu.au
Ihor KuzPrincipal OS Engineer, Kry10 LtdVerified email at ikuz.org
Liam O'ConnorThe Australian National University and The University of EdinburghVerified email at anu.edu.au
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
Kai Engelhardtn.a.Verified email at acm.org
Peter GammieANUVerified email at anu.edu.au
Daniel MatichukPhD Graduate, UNSWVerified email at unswalumni.com
Matthew FernandezIntel LabsVerified email at intel.com
Yutaka NagashimaInstitute of Computer Science, the Czech Academy of SciencesVerified email at cs.cas.cz
Mark StaplesData61, CSIROVerified email at data61.csiro.au
David GreenawayNICTA and School of Computer Science, University of New South WalesVerified email at cse.unsw.edu.au
R JefferyUNSWVerified email at cse.unsw.edu.au

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	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

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