Skip to main content

Gerwin Klein

Gerwin Klein
Senior Principal Reseacher; Conjoint Professor, UNSW

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.

Contact Details

Phone: +61 2 8306 0578
Email:Gerwin.Klein@nicta.com.au
Web:http://www.cse.unsw.edu.au/~kleing
Twitter:@lsf37
Blog:http://proofcraft.org

More contact information is available at the Contact page.

Photo of Gerwin Klein

Publication List

Projects

Current

Past

Gerwin is leading the Trustworthy Systems Research Group at Data61, and was previously leading the formal verification part of the Trustworthy Embedded Systems project, as well as the L4.verified project at NICTA.

Qualifications

Gerwin holds a PhD in Computer Science from Technische Universitaet Muenchen.

Affiliations

Gerwin is Conjoint Full Professor at the School of Computer Science and Engineering at UNSW.

He is also the author and maintainer of the open source Java lexer generator JFlex.

Steering Committees

  • Software Systems Verification (SSV, since 2008)
  • Interactive Theorem Proving (ITP, 2014-2015)
  • Certified Proofs and Programs (CPP, 2012-2013)

Program Committees and Editorial Boards

  • Interactive Theorem Proving (ITP'10, ITP'11, ITP'12, ITP'13, ITP'14 co-chair, ITP'15, ITP'16)
  • Theorem Proving in Higher-Order Logics (TPHOLs'09)
  • International Symposium on Automated Technology for Verification and Analysis (ATVA'13)
  • VeriSure: Verification and Assurance (VeriSure’13)
  • Certified Proofs and Programs (CPP'12)
  • PROOFS: Security Proofs for Embedded Systems (PROOFS’12, PROOFS’13)
  • Verified Software: Theories, Tools and Experiments (VSTTE'11, VSTTE'12, VSTTE'13)
  • 17th International Symposium on Formal Methods (FM'11)
  • International Conference on Formal Engineering Methods (ICFME'10, ICFME'11, ICFEM'12)
  • Formal Methods in Computer Aided Design (FMCAD'10, FMCAD'11)
  • 18th International Workshop on Model Checking of Software (SPIN'11)
  • 20th European Symposium on Programming (ESOP'11)
  • Modules and Libraries for Proof Assistants (MLPA'11)
  • Specification and Verification of Component-Based Systems (SAVCBS'10)
  • Second Workshop on Practical Aspects of Automated Reasoning (PAAR 2010)
  • 6th International Verification Workshop (VERIFY'10)
  • 5th International Verification Workshop (VERIFY'08), co-chair
  • International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09, BYTECODE'10)
  • International Workshop on System Software Verification (SSV'06, SSV'08, SSV'09, SSV'10, SSV'12), co-chair
  • Journal of Automated Reasoning (JAR), guest editor for special issue 2008
  • 10th Workshop on Formal Techniques for Java-like Programs (FTfJP'08)
  • 2nd Inf. ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM'07)
  • 1st Int. Workshop on Microkernels for Embedded Systems (MIKES'07)
  • NICTA Workshop on Operating Systems Verification (OSV'04, chair)
  • Editor for the Archive of Formal Proofs (AFP) since 2004

Recognition and Awards

  • 2012 (with Bourke, Daum, Kolanski): CICM'12 Best Paper Award.
  • 2011 (with L4.verified team): MIT TR10, Top 10 emerging technologies in 2010.
  • 2011 (with L4.verified team): Finalist for Australian Museum Eureka Prize in Computer Science.
  • 2009 (with L4.verfied team): SOSP'09 Best Paper Award.
  • 2004: German Association for Informatics (GI): Best PhD thesis of 2003 in Germany, Austria, Switzerland.
  • 1999: Siemens Award: top four graduates in 1999 at TU Munich.

Publications

Best Papers

Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Abstract
Slides
PDF Thomas Sewell, Magnus Myreen and Gerwin Klein
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471-481, Seattle, Washington, USA, June, 2013
Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415-429, San Francisco, CA, May, 2013
Abstract PDF Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325-340, Nijmegen, The Netherlands, August, 2011
Abstract
Slides
PDF
Presentation Video
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
ACM Symposium on Operating Systems Principles, pp. 207-220, Big Sky, MT, USA, October, 2009
Abstract PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97-108, Nice, France, January, 2007


NICTA Papers

2016

Abstract PDF Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein
Refinement through restraint: Bringing down the cost of verification
International Conference on Functional Programming, Nara, Japan, September, 2016
Abstract PDF Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein
A framework for the automatic formal verification of refinement from Cogent to C
International Conference on Interactive Theorem Proving, Nancy, France, August, 2016
Abstract PDF Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein and Gernot Heiser
Cogent: verifying high-assurance file system implementations
International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 175-188, Atlanta, GA, USA, April, 2016

2015

Abstract PDF Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz
Automated verification of a component platform
Technical Report, NICTA and UNSW, August, 2015
Abstract
Slides
PDF Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz
Automated verification of RPC stub code
International Symposium on Formal Methods, pp. 273-290, Oslo, Norway, June, 2015
Abstract PDF Daniel Matichuk, Toby Murray, June Andronick, Ross Jeffery, Gerwin Klein and Mark Staples
Empirical study towards a leading indicator for cost of formal software verification
International Conference on Software Engineering, pp. 11, Firenze, Italy, February, 2015
Abstract PDF Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein and Toby Murray
An empirical research agenda for understanding formal methods productivity
Information and Software Technology, Volume 60, pp. 102-112, January, 2015

2014

Abstract PDF Matthias Daum, Nelson Billing and Gerwin Klein
Concerned with the unprivileged: User programs in kernel refinement
Formal Aspects of Computing, Volume 26, Number 6, pp. 1205-1229, October, 2014
Abstract PDF Liam O'Connor-Davis, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah
CDSL version 1: Simplifying verification with linear types
Technical Report, NICTA, October, 2014
Abstract PDF Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein and Rafal Kolanski
Productivity for proof engineering
Empirical Software Engineering and Measurement, pp. 15, Turin, Italy, September, 2014
Abstract PDF Daniel Potts, Rene Bourquin, Leslie Andresen, June Andronick, Gerwin Klein and Gernot Heiser
Mathematically verified software kernels: Raising the bar for high assurance implementations
Technical Report, NICTA, July, 2014
Abstract PDF David Greenaway, Japheth Lim, June Andronick and Gerwin Klein
Don't sweat the small stuff: Formal verification of C code without the pain
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 429–439, Edinburgh, UK, June, 2014
Abstract PDF Gerwin Klein
Proof engineering challenges for large-scale verification
Abstract, AI4FM/2014 Workshop.
Abstract PDF Gerwin Klein and Tobias Nipkow
Applications of interactive proof to data flow analysis and security
Software Systems Safety, pp. 77-134, Volume 36 in NATO Science for Peace and Security Series , IOS Press BV, 2014
Abstract
Slides
PDF Gerwin Klein
Proof engineering considered essential
International Symposium on Formal Methods (FM), pp. 16-21, Singapore, April, 2014
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014

2013

Abstract PDF Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
PDF Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick
Towards a verified component platform
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Farmington, PA, USA, November, 2013
Abstract PDF Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
PDF Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor-Davis, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser
File systems deserve verification too!
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Farmington, Pennsylvania, USA, November, 2013
A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 58-64.
Abstract
Slides
PDF Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis and Thomas Sewell
Formally verified system initialisation
International Conference on Formal Engineering Methods, pp. 70-85, Queenstown, New Zealand, October, 2013
Abstract
Slides
PDF Thomas Sewell, Magnus Myreen and Gerwin Klein
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471-481, Seattle, Washington, USA, June, 2013
Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415-429, San Francisco, CA, May, 2013
Abstract PDF Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby Murray, Ross Jeffery and Len Bass
Formal specifications better than function points for code sizing
International Conference on Software Engineering, pp. 1257-1260, San Francisco, USA, May, 2013

2012

Abstract PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein
Noninterference for operating system kernels
International Conference on Certified Programs and Proofs, pp. 126-142, Kyoto, Japan, December, 2012
Abstract PDF June Andronick, Andrew Boyton and Gerwin Klein
Final report for AOARD grant #FA2386-11-1-4070, formal system verification - extension
Technical Report, NICTA, October, 2012
Abstract PDF June Andronick, Gerwin Klein and Toby Murray
Formal system verification for trustworthy embedded systems, final report for AOARD grant #FA2386-10-1-4105
Technical Report, NICTA, October, 2012
Abstract PDF Matthew Fernandez, Ihor Kuz and Gerwin Klein
Formalisation of a component platform
Poster presented at Operating Systems Design and Implementation 2012, October, 2012
Abstract PDF Nick Barnes, Peter Baumgartner, Tiberio Caetano, Hugh Durrant-Whyte, Gerwin Klein, Penelope Sanderson, Abdul Sattar, Peter Stuckey, Sylvie Thiebaux, Pascal Van Hentenryck and Toby Walsh
AI @ NICTA
AI Magazine, Volume 33, Number 3, pp. 115-127, September, 2012
Abstract PDF June Andronick and Gerwin Klein
Formal system verification - extension 2, final report AOARD #FA2386-12-1-4022
Technical Report, NICTA, August, 2012
Abstract PDF David Greenaway, June Andronick and Gerwin Klein
Bridging the gap: Automatic verified abstraction of C
International Conference on Interactive Theorem Proving, pp. 99-115, Princeton, New Jersey, USA, August, 2012
Abstract PDF Gerwin Klein, Rafal Kolanski and Andrew Boyton
Mechanised separation algebra
International Conference on Interactive Theorem Proving, pp. 332-337, Princeton, USA, August, 2012
Abstract PDF Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski
Challenges and experiences in managing large-scale proofs
Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management, pp. 32-48, Bremen, Germany, July, 2012
Abstract PDF June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, Jason Zhang and Liming Zhu
Large-scale formal verification in practice: A process perspective
International Conference on Software Engineering, pp. 1002-1011, Zurich, Switzerland, June, 2012
Abstract PDF Jason Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu and Rafal Kolanski
Simulation modeling of a large scale formal verification process
International Conference on Software and Systems Process, pp. 3-12, Zurich, Switzerland, June, 2012
Abstract PDF June Andronick, Gerwin Klein and Andrew Boyton
Formal system verification - extension, AOARD 114070
Technical Report, NICTA, May, 2012
Abstract PDF Matthew Fernandez, Gerwin Klein and Ihor Kuz
Microkernel verification down to assembly
Poster presented at EuroSys 2012, April, 2012
Abstract PDF Gerwin Klein
Interactive proof: Applications to semantics
Software Safety and Security: Tools for Analysis and Verification, pp. 85-125, IOS Press, 2012
Abstract PDF Gernot Heiser, Toby Murray and Gerwin Klein
It's time for trustworthy systems
IEEE: Security and Privacy, Volume 10, Number 2, pp. 67-70, March, 2012

2011

Abstract PDF June Andronick, Gerwin Klein and Toby Murray
Formal system verification for trustworthy embedded systems, final report option 1 – AOARD 104105
Technical Report, NICTA, November, 2011
Abstract PDF Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325-340, Nijmegen, The Netherlands, August, 2011
Abstract PDF Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood
Provable security: How feasible is it?
Workshop on Hot Topics in Operating Systems, pp. 5, Napa, USA, May, 2011
Abstract PDF June Andronick and Gerwin Klein
Formal system verification for trustworthy embedded systems, final report AOARD 094160
Technical Report, NICTA, April, 2011

2010

Abstract PDF Gerwin Klein
From a verified kernel towards verified systems
Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS), pp. 21–33, Shanghai, China, November, 2010
Invited extended abstract.
Abstract PDF Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk
The road to trustworthy systems
ACM Workshop on Scalable Trusted Computing (ACMSTC), pp. 3-10, Chicago, IL, USA, October, 2010
Abstract PDF Gerwin Klein
The L4.verified project - next steps
Proceedings of Verified Software: Theories, Tools and Experiments 2010, pp. 86–96, Edinburgh, UK, August, 2010
Invited extended abstract.
Abstract PDF Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker
capDL: A language for describing capability-based systems
Asia-Pacific Workshop on Systems (APSys), pp. 31-35, New Delhi, India, August, 2010
Abstract PDF Gerwin Klein
A formally verified OS kernel. Now what?
Proceedings of the 1st International Conference on Interactive Theorem Proving, pp. 1–7, Edinburgh, UK, July, 2010
Invited extended abstract.
Abstract PDF 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 operating-system kernel
Communications of the ACM, Volume 53, Number 6, pp. 107-115, June, 2010
Research Highlights paper
Abstract PDF Gerwin Klein, Thomas Sewell and Simon Winwood
Refinement in the formal verification of seL4
Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 323-339, Springer, 2010

2009

Abstract PDF Gerwin Klein
Correct OS kernel? Proof? Done!
USENIX ;login:, Volume 34, Number 6, pp. 28–34, December, 2009
Abstract PDF Ralf Huuck, Gerwin Klein and Schlich Bastian
Proc. 4th international workshop on system software verification (SSV09)
Electronic Notes in Theoretical Computer Science, Volume 254, pp. 1-3, October, 2009
Abstract
Slides
PDF
Presentation Video
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
ACM Symposium on Operating Systems Principles, pp. 207-220, Big Sky, MT, USA, October, 2009
Abstract PDF
Presentation Video
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, pp. 91–96, Edinburgh, UK, August, 2009
Abstract PDF Rafal Kolanski and Gerwin Klein
Types, maps and separation logic
International Conference on Theorem Proving in Higher Order Logics, pp. 276-292, Munich, Germany, August, 2009
Abstract PDF Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish
Mind the gap: A verification framework for low-level C
International Conference on Theorem Proving in Higher Order Logics, pp. 500-515, Munich, Germany, August, 2009
Abstract PDF Gerwin Klein, Ralf Huuck and Bastian Schlich
Operating system verification
Volume 42, Number 2-4, pp. 1-2, May, 2009
Abstract PDF Gerwin Klein
Operating system verification — an overview
Sādhanā, Volume 34, Number 1, pp. 27–69, February, 2009
Invited paper. Journal homepage.

2008

Abstract PDF Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Verified Software: Theories, Tools and Experiments, pp. 99–115, Toronto, Canada , October, 2008
Abstract PDF Rafal Kolanski and Gerwin Klein
Mapped separation logic
Verified Software: Theories, Tools and Experiments, pp. 15-29, Toronto, Canada, October, 2008
Abstract PDF Bernhard Beckert and Gerwin Klein
5th international verification workshop – VERIFY'08
CEUR Workshop Proceedings, 2008
Abstract PDF 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, pp. 167-182, Montreal, Canada, August, 2008
Abstract PDF Ralf Huuck, Gerwin Klein and Bastian Schlich
Proceedings of the 3rd international workshop on systems software verification (SSV 2008)
Volume 217 in ENTCS, Elsevier, 2008

2007

Abstract PDF Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan Petters
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, Volume 41, Number 4, pp. 3-11, December, 2007
Abstract PDF Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Technical Report NRL-1474, NICTA, October, 2007
Abstract PDF Jia Meng, Lawrence C. Paulson and Gerwin Klein
A termination checker for isabelle hoare logic
International Verification Workshop, pp. 104-118, Bremen, Germany, July, 2007
Abstract PDF Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser
Towards a practical, verified kernel
Workshop on Hot Topics in Operating Systems, pp. 6, San Diego, CA, USA, May, 2007
Abstract PDF 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
Abstract PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97-108, Nice, France, January, 2007

2006

Abstract PDF 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
Abstract PDF Kevin Elphinstone, Gerwin Klein and Rafal Kolanski
Formalising a high-performance microkernel
Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), pp. 1-7, Seattle, USA, August, 2006
Abstract PDF Gerwin Klein and Rafal Kolanski
Formalising the L4 microkernel API
Computing: The Australasian Theory Symposium (CATS), pp. 53–68, Hobart, Australia, January, 2006
Abstract PDF Gerwin Klein and Tobias Nipkow
A machine-checked model for a Java-like language, virtual machine, and compiler
ACM Transactions on Programming Languages and Systems, Volume 28, Number 4, pp. 619–695, 2006
Abstract PDF 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, pp. 111–126, Venice, Italy, 2006

2005

Abstract PDF 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, pp. 474–488, Montego Bay, Jamaica, December, 2005
Abstract PDF Harvey Tuch, Gerwin Klein and Gernot Heiser
OS verification — now!
Proceedings of the 10th Workshop on Hot Topics in Operating Systems, pp. 7–12, Santa Fe, NM, USA, June, 2005

2004

Abstract PDF Harvey Tuch and Gerwin Klein
Verifying the L4 virtual memory subsystem
Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, pp. 73–97, Sydney, Australia, October, 2004
Abstract PDF Gerwin Klein and Harvey Tuch
Towards verified virtual memory in L4
TPHOLs Emerging Trends '04, pp. 16 pages, Park City, Utah, USA, September, 2004

Non-NICTA Papers

2005

plain text link Gerwin Klein
Verified java bytecode verification
it - Information Technology, Volume 47, pp. 107–110, 2005

2004

plain text link Martin Wildmoser, Tobias Nipkow, Gerwin Klein and Sebastian Nanz
Prototyping proof carrying code
Proc. 3rd IFIP Int. Conf. Theoretical Computer Science (TCS 2004), pp. 333–348, Toulouse, France, August, 2004
plain text link Gerwin Klein and Martin Strecker
Verified Bytecode Verification and type-certifying Compilation
Journal of Logic and Algebraic Programming, Volume 58, Number 1–2, pp. 27–60, 2004

2003

plain text link Gerwin Klein and Martin Wildmoser
Verified bytecode subroutines
Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics, pp. 55–70, Rome, Italy, September, 2003
plain text link Gerwin Klein
Verified java bytecode verification
PhD Thesis, Institut für Informatik, Technische Universität München, 2003
plain text link Gerwin Klein and Tobias Nipkow
Verified bytecode verifiers
Theoretical Computer Science, Volume 3, Number 298, pp. 583–626, 2003
plain text link Gerwin Klein and Martin Wildmoser
Verified bytecode subroutines
Journal of Automated Reasoning, Volume 30, Number 3–4, pp. 363–398, 2003

2001

plain text link Gerwin Klein and Tobias Nipkow
Verified lightweight bytecode verification
Concurrency and Computation: Practice and Experience, Volume 13, Number 13, pp. 1133–1151, 2001

2000

plain text to be published Gerwin Klein and Tobias Nipkow
Verified lightweight bytecode verification
Proc. 2nd ECOOP Workshop on Formal Techniques for Java Programs (TR 269, Fernuniversität Hagen), pp. 35–42, Cannes, France, 2000

1999

plain text to be published Alfons Brandl and Gerwin Klein
Formgen: A generator for adaptive forms based on easygui
Proceedings of the 8th International Conference on Human-Computer Interaction: Ergonomics and User Interfaces (HCI), pp. 1172–1176, Munich, Germany, August, 1999

1998

plain text link Gerwin Klein
JFlex: The fast lexical analyzer generator for Java
1998

Research Theses Supervised

2014

Abstract PDF Andrew Boyton
Secure architectures on a verified microkernel
PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014