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:/ |
| Twitter: | @lsf37 |
| Blog: | http:/ |
More contact information is available at the Contact page.
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
- Google Scholar profile
- Best Papers
- TS Group Papers (2023, 2022, 2020, 2019, 2018, 2017, 2016, 2015, 2014, 2013, 2012, 2011, 2010, 2009, 2008, 2007, 2006, 2005, 2004)
- Papers not affiliated with TS (2005, 2004, 2003, 2001, 2000, 1999, 1998)
- Research Theses Supervised
Best Papers
|
 |
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 |
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
 |
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 |
|
|
|
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
|
|
|
Rob 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 |
|
|
|
Scott Buckley, Rob 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
|
|
|
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 |
|
|
|
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
|
|
|
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
|
|
|
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 |
|
|
 |
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 |
|
|
|
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
|
|
|
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
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Hira Taqdees Syeda and Gerwin Klein Reasoning about translation lookaside buffers International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 490–508, Maun, Botswana, May, 2017 |
2016
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz Automated verification of a component platform Technical Report, NICTA and UNSW, August, 2015 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Gerwin Klein Proof engineering challenges for large-scale verification Abstract, AI4FM/2014 Workshop. |
|
|
|
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 |
|
|
|
Gerwin Klein Proof engineering considered essential International Symposium on Formal Methods (FM), pp. 16–21, Singapore, April, 2014 |
|
|
|
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
|
|
|
Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz CAmkES glue code semantics Technical Report, NICTA and UNSW, November, 2013 |
|
|
|
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 |
|
|
|
Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray CAmkES formalisation of a component platform Technical Report, NICTA and UNSW, November, 2013 |
|
|
|
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. |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Matthew Fernandez, Ihor Kuz and Gerwin Klein Formalisation of a component platform Poster presented at Operating Systems Design and Implementation 2012, October, 2012 |
|
|
|
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 |
|
|
|
June Andronick and Gerwin Klein Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022 Technical Report, NICTA, August, 2012 |
|
|
|
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 |
|
|
|
Gerwin Klein, Rafal Kolanski and Andrew Boyton Mechanised separation algebra International Conference on Interactive Theorem Proving, pp. 332–337, Princeton, USA, August, 2012 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
June Andronick, Gerwin Klein and Andrew Boyton Formal system verification — extension, AOARD 114070 Technical Report, NICTA, May, 2012 |
|
|
|
Matthew Fernandez, Gerwin Klein and Ihor Kuz Microkernel verification down to assembly Poster presented at EuroSys 2012, April, 2012 |
|
|
|
Gerwin Klein Interactive proof: Applications to semantics Software Safety and Security: Tools for Analysis and Verification, pp. 85–125, IOS Press, 2012 |
|
|
|
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
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
June Andronick and Gerwin Klein Formal system verification for trustworthy embedded systems, final report AOARD 094160 Technical Report, NICTA, April, 2011 |
2010
|
|
|
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. |
|
|
|
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 |
|
|
|
Gerwin Klein The l4.verified project – next steps Verified Software: Theories, Tools and Experiments, pp. 86–96, Edinburgh, UK, August, 2010 |
|
|
|
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 |
|
|
|
Gerwin Klein A formally verified OS kernel. now what? International Conference on Interactive Theorem Proving, pp. 1–7, Edinburgh, UK, July, 2010 |
|
|
|
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 |
|
|
|
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
|
|
|
Gerwin Klein Correct OS kernel? Proof? Done! USENIX ;login:, Volume 34, Number 6, pp. 28–34, December, 2009 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Gerwin Klein, Ralf Huuck and Bastian Schlich Operating system verification Journal of Automated Reasoning, Volume 42, Number 2-4, pp. 123–124, April, 2009 |
|
|
|
Gerwin Klein Operating system verification — an overview Sadhana, Volume 34, Number 1, pp. 26–69, February, 2009 Invited paper. Journal homepage. |
2008
|
|
|
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 |
|
|
|
Rafal Kolanski and Gerwin Klein Mapped separation logic Verified Software: Theories, Tools and Experiments, pp. 15–29, Toronto, Canada, October, 2008 |
|
|
|
5th international verification workshop — VERIFY'08 CEUR Workshop Proceedings, 2008 |
|
|
|
David Cock, Gerwin Klein and Thomas Sewell Secure microkernels, state monads and scalable refinement International Conference on Theorem Proving in Higher Order Logics, pp. 167–182, Montreal, Canada, August, 2008 |
|
|
|
Proceedings of the 3rd international workshop on systems software verification (SSV 2008) Volume 217 in ENTCS, Elsevier, 2008 |
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, Volume 41, Number 4, pp. 3–11, December, 2007 |
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Technical Report NRL-1474, NICTA, October, 2007 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser Verifying a high-performance micro-kernel Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007 |
|
|
|
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
|
|
|
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 Verified Software: Theories, Tools and Experiments, pp. 1-7, Seattle, USA, August, 2006 |
|
|
|
Gerwin Klein and Rafal Kolanski Formalising the L4 microkernel API Computing: The Australasian Theory Symposium (CATS), pp. 53–68, Hobart, Australia, January, 2006 |
|
|
|
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 |
|
|
|
Simon Winwood, Gerwin Klein and Manuel Chakravarty On the synthesis of proof-carrying temporal reference monitors International Symposium on Logic-Based Program Synthesis and Transformation, pp. 111–126, Venice, Italy, 2006 |
2005
|
|
|
Harvey Tuch and Gerwin Klein A unified memory model for pointers International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 474–488, Montego Bay, Jamaica, December, 2005 |
|
|
|
Harvey Tuch, Gerwin Klein and Gernot Heiser OS verification — now! Workshop on Hot Topics in Operating Systems (HotOS), pp. 7–12, 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, pp. 73–97, Sydney, Australia, October, 2004 |
|
|
|
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
 |
Gerwin Klein Verified java bytecode verification it - Information Technology, Volume 47, Issue 2, pp. 107–110, 2005 |
2004
|
|
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 | |
|
|
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
|
|
Gerwin Klein and Martin Wildmoser Verified bytecode subroutines International Conference on Theorem Proving in Higher Order Logics, pp. 55–70, Rome, Italy, September, 2003 | |
|
|
Gerwin Klein Verified java bytecode verification PhD Thesis, Institut für Informatik, Technische Universität München, 2003 | |
|
|
Gerwin Klein and Tobias Nipkow Verified bytecode verifiers Theoretical Computer Science, Volume 3, Number 298, pp. 583–626, 2003 | |
|
|
Gerwin Klein and Martin Wildmoser Verified bytecode subroutines Journal of Automated Reasoning, Volume 30, Number 3–4, pp. 363–398, 2003 |
2001
|
|
Gerwin Klein and Tobias Nipkow Verified lightweight bytecode verification Concurrency and Computation: Practice and Experience, Volume 13, Number 13, pp. 1133–1151, 2001 |
2000
|
|
|
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
|
|
|
Alfons Brandl and Gerwin Klein Formgen: A generator for adaptive forms based on easygui International Conference on Human-Computer Interaction: Ergonomics and User Interfaces (HCI), pp. 1172–1176, Munich, Germany, August, 1999 |
1998
|
|
Gerwin Klein JFlex: The fast lexical analyzer generator for Java 1998 |
Research Theses Supervised
2019
|
|
|
Hira Taqdees Syeda Low-level program verification under cached address translation PhD Thesis, UNSW, Sydney, Australia, August, 2019 |
2018
|
|
|
Daniel Matichuk Automation for proof engineering: Machine-checked proofs at scale PhD Thesis, UNSW, Sydney, Australia, July, 2018 |
2017
|
|
|
Thomas Sewell Translation validation for verified, efficient and timely operating systems PhD Thesis, UNSW, Sydney, Australia, July, 2017 |
2016
|
|
|
Matthew Fernandez Formal verification of a component platform PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016 |
2015
|
|
|
David Greenaway Automated proof-producing abstraction of c code PhD Thesis, CSE, UNSW, Sydney, Australia, March, 2015 |
2014
|
|
|
Andrew Boyton Secure architectures on a verified microkernel PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014 |
2011
|
|
|
Rafal Kolanski Verification of programs in virtual memory using separation logic PhD Thesis, UNSW, Sydney, Australia, July, 2011 |
2008
|
|
|
Harvey Tuch Formal memory models for verifying C systems code PhD Thesis, UNSW, Sydney, Australia, August, 2008 |