Trustworthy Systems

Gerwin Klein
Adjunct Professor; Founder and Chief Scientist at Proofcraft

Research Interests

Gerwin's research interest is in Formal Methods, more specifically in interactive theorem proving, software verification, semantics of programming languages, and in the emerging field of proof engineering. Generally, he wants software systems to be dependable, and thinks that formal specification and proof can make a significant contribution towards that goal.

Contact Details

Email:kleing@unsw.edu.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


Gerwin is the Chief Scientist of Proofcraft

Projects

Current

Past

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.

Grants

Multiple grants from AOARD and DARPA.

Recognition and Awards

  • 2019 (with L4.verfied team): SIGOPs Hall of Fame Award for seL4
  • 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
Best Paper Award
Hall of Fame Award
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


Trustworthy Systems Group Papers

2023

Abstract
Slides
PDF Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein and Gernot Heiser
Formalising the prevention of microarchitectural timing channels by operating systems
International Symposium on Formal Methods (FM), Lübeck, DE, March, 2023
Abstract PDF Scott Buckley, Robert Sison, Nils Wistoff, Curtis Millar, Toby Murray, Gerwin Klein and Gernot Heiser
Proving the absence of microarchitectural timing channels
arXiv preprint arXiv:2310.17046, 2023

2022

Abstract PDF Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser and Gabriele Keller
Property-based testing: Climbing the stairway to verification
ACM SIGPLAN International Conference on Software Language Engineering, Auckland, New Zealand, December, 2022
Distinguished Artifact Award
Abstract PDF Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer and John Shackleton
Cyberassured systems engineering at scale
IEEE Security and Privacy, Volume 20, Number 3, pp. 52–64, March, 2022

2021

Abstract PDF Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell and Gabriele Keller
Cogent: Uniqueness types and certifying compilation
Journal of Functional Programming, Volume 31, 2021

2020

Abstract PDF Gernot Heiser, Toby Murray and Gerwin Klein
Towards provable timing-channel prevention
ACM Operating Systems Review, Volume 54, Issue 1, pp. 1-7, August, 2020
Abstract to be published Hira Taqdees Syeda and Gerwin Klein
Formal reasoning under cached address translation
Journal of Automated Reasoning, Volume 64, Issue 6, pp. 911-945, June, 2020
Abstract PDF Gernot Heiser, Gerwin Klein and June Andronick
seL4 in Australia: From research to real-world trustworthy systems
Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020

2019

Abstract PDF Gernot Heiser, Gerwin Klein and Toby Murray
Can we prove time protection?
Workshop on Hot Topics in Operating Systems (HotOS), pp. 23-29, Bertinoro, Italy, May, 2019

2018

Abstract PDF Darren Cofer, Andrew Gacek, John Backes, Michael Whalen, Lee Pike, Adam Foltzer, Michael Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser and Douglas Stuart
A formal approach to constructing secure air vehicle software
IEEE Computer, Volume 51, Issue 11, pp. 14-23, November, 2018
Abstract PDF Liam O'Connor, Zilin Chen, Partha Susarla Ajay, Christine Rizkallah, Gerwin Klein and Gabriele Keller
Bringing effortless refinement of data layouts to Cogent
International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, pp. 134-149, Limassol, Cyprus, November, 2018
Abstract PDF Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez
Formally verified software in the real world
Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018
Abstract PDF Callum Bannister, Peter Hoefner and Gerwin Klein
Backwards and forwards with separation logic
International Conference on Interactive Theorem Proving, pp. 68–87, Oxford, July, 2018
Abstract PDF Hira Taqdees Syeda and Gerwin Klein
Program verification in the presence of cached address translation
International Conference on Interactive Theorem Proving, pp. 542-559, Oxford, UK, July, 2018

2017

Abstract PDF Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein and Gernot Heiser
The Cogent case for property-based testing
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Shanghai, China, October, 2017
Abstract PDF Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson
Secure mathematically-assured composition of control models
Technical Report, Data61, CSIRO, September, 2017
Abstract PDF Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray and Liam O'Connor
Provably trustworthy systems
Philosophical Transactions of the Royal Society A, Volume 375, Issue 2104, pp. 1-23, September, 2017
Abstract PDF Hira Taqdees Syeda and Gerwin Klein
Reasoning about translation lookaside buffers
Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 490–508, Maun, Botswana, May, 2017

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 (FM), 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, 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, 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
Proceedings of the 15th 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 Symposium on 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 (HotOS), 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
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
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?
International Conference on Interactive Theorem Proving, pp. 1–7, Edinburgh, UK, July, 2010
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
Best Paper Award
Hall of Fame Award
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 Gerwin Klein, Philip Derrin and Kevin Elphinstone
Experience report: seL4 – formally verifying a high-performance microkernel
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
Journal of Automated Reasoning, Volume 42, Number 2-4, pp. 123–124, April, 2009
Abstract PDF Gerwin Klein
Operating system verification — an overview
Sadhana, Volume 34, Number 1, pp. 26–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 M. 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 (HotOS), 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
Verified Software: Theories, Tools and Experiments, 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 (HotOS), 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

Papers without TS Affiliation

2005

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

2004

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

  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
  link Gerwin Klein
Verified java bytecode verification
PhD Thesis, Institut für Informatik, Technische Universität München, 2003
  link Gerwin Klein and Tobias Nipkow
Verified bytecode verifiers
Theoretical Computer Science, Volume 3, Number 298, pp. 583–626, 2003
  link Gerwin Klein and Martin Wildmoser
Verified bytecode subroutines
Journal of Automated Reasoning, Volume 30, Number 3–4, pp. 363–398, 2003

2001

  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

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

Research Theses Supervised

2019

Abstract to be published Hira Taqdees Syeda
Low-level program verification under cached address translation
PhD Thesis, UNSW, Sydney, Australia, August, 2019

2018

Abstract PDF Daniel Matichuk
Automation for proof engineering: Machine-checked proofs at scale
PhD Thesis, UNSW, Sydney, Australia, 2018

2017

Abstract PDF Thomas Sewell
Translation validation for verified, efficient and timely operating systems
PhD Thesis, UNSW, Sydney, Australia, 2017

2016

Abstract PDF Matthew Fernandez
Formal verification of a component platform
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016

2015

Abstract PDF David Greenaway
Automated proof-producing abstraction of c code
PhD Thesis, CSE, UNSW, Sydney, Australia, March, 2015

2014

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

2011

Abstract PDF Rafal Kolanski
Verification of programs in virtual memory using separation logic
PhD Thesis, UNSW, Sydney, Australia, July, 2011

2008

Abstract PDF Harvey Tuch
Formal memory models for verifying C systems code
PhD Thesis, UNSW, Sydney, Australia, August, 2008