Gerwin Klein - Principal Researcher
Trustworthy Embedded Systems Project
Research Interests
Gerwin's research interest is in Formal Methods, more specifically in interactive theorem proving, software verification, and semantics of programming languages. Generally, he wants software systems to be dependable, and thinks that formal specification and proof can make a very significant contribution towards that goal.
NICTA Projects
Gerwin is leading the L4.verified project at NICTA.
Qualifications
Gerwin holds a PhD in Computer Science from Technische Universitaet Muenchen.
Contact Details
| Email: | gerwin.klein@nicta.com.au |
|---|---|
| Web: | http://www.cse.unsw.edu.au/~kleing/ |
More contact information is available at the ERTOS Contacts page.
Publications
Best Papers
|
 |
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel Communications of the ACM, 53(6), 107–115, (June, 2010) |
|
|
|
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009 Best Paper Award! |
|
|
|
Harvey Tuch, Gerwin Klein and Michael Norrish Types, bytes, and separation logic Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007 |
NICTA Papers
2010
|
|
|
Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk The road to trustworthy systems Proceedings of the 5th Workshop on Scalable Trusted Computing, Chicago, IL, USA, October, 2010 Invited paper |
|
|
|
Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Walker capDL: A language for describing capability-based systems Proceedings of the 1st Asia-Pacific Workshop on Systems, New Delhi, India, August, 2010 To appear |
|
|
|
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel Communications of the ACM, 53(6), 107–115, (June, 2010) |
2009
|
|
|
Gerwin Klein Correct OS kernel? Proof? Done! USENIX ;login:, 34(6), 28–34, (December, 2009) |
|
|
|
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood seL4: Formal verification of an OS kernel Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009 Best Paper Award! |
|
|
|
Gerwin Klein, Philip Derrin and Kevin Elphinstone Experience report: seL4 — formally verifying a high-performance microkernel Proceedings of the 14th International Conference on Functional Programming, Edinburgh, UK, August, 2009 |
|
|
|
Rafal Kolanski and Gerwin Klein Types, maps and separation logic Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August, 2009 |
|
|
|
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish Mind the gap: A verification framework for low-level C Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August, 2009 |
|
|
|
Gerwin Klein Operating system verification — an overview Sādhanā, 34(1), 27–69, (February, 2009) Invited paper. Journal homepage. |
2008
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Proceedings of Verified Software: Theories, Tools and Experiments 2008, Toronto, Canada, October, 2008 |
|
|
|
Rafal Kolanski and Gerwin Klein Mapped separation logic Proceedings of Verified Software: Theories, Tools and Experiments 2008, Toronto, Canada, October, 2008 |
|
|
|
David Cock, Gerwin Klein and Thomas Sewell Secure microkernels, state monads and scalable refinement Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, Montreal, Canada, August, 2008 |
2007
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Technical Report NRL-1474, NICTA, October, 2007 |
|
|
|
Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters Towards trustworthy computing systems: Taking microkernels to the next level ACM Operating Systems Review, 41(4), 3–11, (July, 2007) |
|
|
|
Jia Meng, Lawrence C. Paulson and Gerwin Klein A termination checker for Isabelle Hoare logic Proceedings of the 4th International Verification Workshop, Bremen, Germany, July, 2007 |
|
|
|
Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser Towards a practical, verified kernel Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007 |
|
|
|
Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser Verifying a high-performance micro-kernel 7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007 |
|
|
|
Harvey Tuch, Gerwin Klein and Michael Norrish Types, bytes, and separation logic Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007 |
2006
|
|
|
Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M. T. Chakravarty Running the manual: An approach to high-assurance microkernel development Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA, September, 2006 |
|
|
|
Kevin Elphinstone, Gerwin Klein and Rafal Kolanski Formalising a high-performance microkernel Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Seattle, USA, August, 2006 |
|
|
|
Rafal Kolanski and Gerwin Klein Formalising the L4 microkernel API Computing: The Australasian Theory Symposium (CATS 06), Hobart, Australia, January, 2006 |
|
|
|
Simon Winwood, Gerwin Klein and Manuel Chakravarty On the synthesis of proof-carrying temporal reference monitors Proceedings of the 16th International Symposium on Logic-Based Program Synthesis and Transformation, Venice, Italy, 2006 |
2005
|
|
|
Harvey Tuch and Gerwin Klein A unified memory model for pointers Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Montego Bay, Jamaica, December, 2005 |
|
|
|
Harvey Tuch, Gerwin Klein and Gernot Heiser OS verification — now! Proceedings of the 10th Workshop on Hot Topics in Operating Systems, Santa Fe, NM, USA, June, 2005 |
2004
|
|
|
Harvey Tuch and Gerwin Klein Verifying the L4 virtual memory subsystem Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004 |
|
|
|
Gerwin Klein and Harvey Tuch Towards verified virtual memory in L4 TPHOLs Emerging Trends '04, Park City, Utah, USA, September, 2004 |
Research Theses Supervised
2008
|
|
|
Harvey Tuch Formal memory models for verifying C systems code, PhD Thesis, School of Computer Science and Engineering, University of NSW, Sydney 2052, Australia, 2008 |