Gerwin Klein

Cited by

	All	Since 2019
Citations	7964	2983
h-index	34	21
i10-index	79	47

600

300

150

450

200320042005200620072008200920102011201220132014201520162017201820192020202120222023202452 44 64 69 108 181 236 336 282 352 411 476 499 589 575 560 589 500 491 528 517 357

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 KuzSenior 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	2835*	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	517	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	371	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	302	2013
Concrete semantics: with Isabelle/HOL T Nipkow, G Klein Springer International Publishing, 2014	299	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	248	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	216	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	149*	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	138	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	135	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	122	2011
Secure microkernels, state monads and scalable refinement D Cock, G Klein, T Sewell Theorem Proving in Higher Order Logics: 21st International Conference …, 2008	114	2008
Verified protection model of the seL4 microkernel D Elkaduwe, G Klein, K Elphinstone Verified Software: Theories, Tools, Experiments: Second International …, 2008	87	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	86	2014
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	84	2012
Bridging the gap: Automatic verified abstraction of C D Greenaway, J Andronick, G Klein Interactive Theorem Proving: Third International Conference, ITP 2012 …, 2012	84	2012
Towards a Practical, Verified Kernel. K Elphinstone, G Klein, P Derrin, T Roscoe, G Heiser HotOS, 2007	67	2007
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	66	2009

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