Gerwin Klein

According to our database, Gerwin Klein authored at least 91 papers between 1999 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

Proving the Absence of Microarchitectural Timing Channels.

Scott Buckley, Robert Sison, Nils Wistoff, Curtis Millar, Toby Murray, Gerwin Klein, Gernot Heiser

CoRR, 2023

Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems.

Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein, Gernot Heiser

Proceedings of the Formal Methods - 25th International Symposium, 2023

2022

Cyberassured Systems Engineering at Scale.

Darren D. Cofer, Isaac Amundson, Junaid Babar, David S. Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer, John Shackleton

IEEE Secur. Priv., 2022

Property-Based Testing: Climbing the Stairway to Verification.

Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser, Gabriele Keller

Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, 2022

2021

Cogent: uniqueness types and certifying compilation.

Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, Gabriele Keller

J. Funct. Program., 2021

2020

Towards Provable Timing-Channel Prevention.

Gernot Heiser, Toby Murray, Gerwin Klein

ACM SIGOPS Oper. Syst. Rev., 2020

Formal Reasoning Under Cached Address Translation.

Hira Taqdees Syeda, Gerwin Klein

J. Autom. Reason., 2020

seL4 in Australia: from research to real-world trustworthy systems.

Gernot Heiser, Gerwin Klein, June Andronick

Commun. ACM, 2020

2019

Can We Prove Time Protection?

Gernot Heiser, Gerwin Klein, Toby C. Murray

Proceedings of the Workshop on Hot Topics in Operating Systems, 2019

2018

Introduction to Milestones in Interactive Theorem Proving.

Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting

J. Autom. Reason., 2018

A Formal Approach to Constructing Secure Air Vehicle Software.

Darren D. Cofer, Andrew Gacek, John Backes, Michael W. Whalen, Lee Pike, Adam Foltzer, Michal Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser, Douglas Stuart

Computer, 2018

Formally verified software in the real world.

Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby C. Murray, Gernot Heiser

Commun. ACM, 2018

Program Verification in the Presence of Cached Address Translation.

Hira Taqdees Syeda, Gerwin Klein

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Backwards and Forwards with Separation Logic.

Callum Bannister, Peter Höfner, Gerwin Klein

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Bringing Effortless Refinement of Data Layouts to Cogent.

Liam O'Connor, Zilin Chen, Partha Susarla, Christine Rizkallah, Gerwin Klein, Gabriele Keller

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Modeling, 2018

2017

The Cogent Case for Property-Based Testing.

Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein, Gernot Heiser

Proceedings of the 9th Workshop on Programming Languages and Operating Systems, 2017

Reasoning about Translation Lookaside Buffers.

Hira Taqdees Syeda, Gerwin Klein

Proceedings of the LPAR-21, 2017

2016

Interactive Theorem Proving - Preface of the Special Issue.

Gerwin Klein, Ruben Gamboa

J. Autom. Reason., 2016

COGENT: Certified Compilation for a Functional Systems Language.

Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, Gerwin Klein

CoRR, 2016

Finite Machine Word Library.

Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk, Thomas Sewell

Arch. Formal Proofs, 2016

A Framework for the Automatic Formal Verification of Refinement from Cogent to C.

Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Refinement through restraint: bringing down the cost of verification.

Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby C. Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

CoGENT: Verifying High-Assurance File System Implementations.

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 C. Murray, Gerwin Klein, Gernot Heiser

Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, 2016

2015

An empirical research agenda for understanding formal methods productivity.

D. Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein, Toby C. Murray

Inf. Softw. Technol., 2015

Qualification of Formal Methods Tools (Dagstuhl Seminar 15182).

Darren D. Cofer, Gerwin Klein, Konrad Slind, Virginie Wiels

Dagstuhl Reports, 2015

Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification.

Daniel Matichuk, Toby C. Murray, June Andronick, D. Ross Jeffery, Gerwin Klein, Mark Staples

Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015

Automated Verification of RPC Stub Code.

Matthew Fernandez, June Andronick, Gerwin Klein, Ihor Kuz

Proceedings of the FM 2015: Formal Methods, 2015

2014

Applications of Interactive Proof to Data Flow Analysis and Security.

Gerwin Klein, Tobias Nipkow

Proceedings of the Software Systems Safety, 2014

Comprehensive formal verification of an OS microkernel.

Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser

ACM Trans. Comput. Syst., 2014

File systems deserve verification too!

Gabriele Keller, Toby C. Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, Gernot Heiser

ACM SIGOPS Oper. Syst. Rev., 2014

Concerned with the unprivileged: user programs in kernel refinement.

Matthias Daum, Nelson Billing, Gerwin Klein

Formal Aspects Comput., 2014

Don't sweat the small stuff: formal verification of C code without the pain.

David Greenaway, Japheth Lim, June Andronick, Gerwin Klein

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

Proof Engineering Considered Essential.

Gerwin Klein

Proceedings of the FM 2014: Formal Methods, 2014

Productivity for proof engineering.

Mark Staples, D. Ross Jeffery, June Andronick, Toby C. Murray, Gerwin Klein, Rafal Kolanski

Proceedings of the 2014 ACM-IEEE International Symposium on Empirical Software Engineering and Measurement, 2014

Concrete Semantics - With Isabelle/HOL

Tobias Nipkow, Gerwin Klein

Springer, ISBN: 978-3-319-10542-0, 2014

2013

seL4: From General Purpose to a Proof of Information Flow Enforcement.

Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, Gerwin Klein

Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Towards a verified component platform.

Matthew Fernandez, Ihor Kuz, Gerwin Klein, June Andronick

Proceedings of the Seventh Workshop on Programming Languages and Operating Systems, 2013

Translation validation for a verified OS kernel.

Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Formal specifications better than function points for code sizing.

Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby C. Murray, D. Ross Jeffery, Len Bass

Proceedings of the 35th International Conference on Software Engineering, 2013

Formally Verified System Initialisation.

Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis, Thomas Sewell

Proceedings of the Formal Methods and Software Engineering, 2013

2012

Interactive Proof: Applications to Semantics.

Gerwin Klein

Proceedings of the Software Safety and Security - Tools for Analysis and Verification, 2012

It's Time for Trustworthy Systems.

Gernot Heiser, Toby C. Murray, Gerwin Klein

IEEE Secur. Priv., 2012

AI@NICTA.

Nick Barnes, Peter Baumgartner, Tibério S. Caetano, Hugh F. Durrant-Whyte, Gerwin Klein, Penelope Sanderson, Abdul Sattar, Peter J. Stuckey, Sylvie Thiébaux, Pascal Van Hentenryck, Toby Walsh

AI Mag., 2012

Separation Algebra.

Gerwin Klein, Rafal Kolanski, Andrew Boyton

Arch. Formal Proofs, 2012

Mechanised Separation Algebra.

Gerwin Klein, Rafal Kolanski, Andrew Boyton

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Bridging the Gap: Automatic Verified Abstraction of C.

David Greenaway, June Andronick, Gerwin Klein

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Simulation modeling of a large-scale formal verification process.

He Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu, Rafal Kolanski

Proceedings of the 2012 International Conference on Software and System Process, 2012

Large-scale formal verification in practice: A process perspective.

June Andronick, D. Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He Zhang, Liming Zhu

Proceedings of the 34th International Conference on Software Engineering, 2012

Noninterference for Operating System Kernels.

Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

Challenges and Experiences in Managing Large-Scale Proofs.

Timothy Bourke, Matthias Daum, Gerwin Klein, Rafal Kolanski

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011

seL4 Enforces Integrity.

Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Provable Security: How Feasible Is It?

Gerwin Klein, Toby C. Murray, Peter Gammie, Thomas Sewell, Simon Winwood

Proceedings of the 13th Workshop on Hot Topics in Operating Systems, 2011

2010

seL4: formal verification of an operating-system kernel.

Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood

Commun. ACM, 2010

The L4.verified Project - Next Steps.

Gerwin Klein

Proceedings of the Verified Software: Theories, 2010

capDL: a language for describing capability-based systems.

Ihor Kuz, Gerwin Klein, Corey Lewis, Adam Walker

Proceedings of the 1st ACM SIGCOMM Asia-Pacific Workshop on Systems, 2010

A Formally Verified OS Kernel. Now What?

Gerwin Klein

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

The road to trustworthy systems.

Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz, Leonid Ryzhyk

Proceedings of the fifth ACM workshop on Scalable trusted computing, 2010

From a Verified Kernel towards Verified Systems.

Gerwin Klein

Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

Refinement in the Formal Verification of the seL4 Microkernel.

Gerwin Klein, Thomas Sewell, Simon Winwood

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009

Correct OS Kernel? Proof? Done!

Gerwin Klein

login Usenix Mag., 2009

Operating System Verification.

Gerwin Klein, Ralf Huuck, Bastian Schlich

J. Autom. Reason., 2009

Mind the Gap.

Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David A. Cock, Michael Norrish

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Types, Maps and Separation Logic.

Rafal Kolanski, Gerwin Klein

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

seL4: formal verification of an OS kernel.

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood

Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

Experience report: seL4: formally verifying a high-performance microkernel.

Gerwin Klein, Philip Derrin, Kevin Elphinstone

Proceedings of the Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, 2009

2008

Preface.

Ralf Huuck, Gerwin Klein, Bastian Schlich

Proceedings of the 3rd International Workshop on Systems Software Verification, 2008

Mapped Separation Logic.

Rafal Kolanski, Gerwin Klein

Proceedings of the Verified Software: Theories, 2008

Verified Protection Model of the seL4 Microkernel.

Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone

Proceedings of the Verified Software: Theories, 2008

Secure Microkernels, State Monads and Scalable Refinement.

David A. Cock, Gerwin Klein, Thomas Sewell

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Title, Preface, Table of Contents.

Bernhard Beckert, Gerwin Klein

Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, 2008

2007

Towards trustworthy computing systems: taking microkernels to the next level.

Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein, Stefan M. Petters

ACM SIGOPS Oper. Syst. Rev., 2007

Types, bytes, and separation logic.

Harvey Tuch, Gerwin Klein, Michael Norrish

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Towards a Practical, Verified Kernel.

Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe, Gernot Heiser

Proceedings of HotOS'07: 11th Workshop on Hot Topics in Operating Systems, 2007

A Termination Checker for Isabelle Hoare Logic.

Jia Meng, Lawrence C. Paulson, Gerwin Klein

Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

2006

A machine-checked model for a Java-like language, virtual machine, and compiler.

Gerwin Klein, Tobias Nipkow

ACM Trans. Program. Lang. Syst., 2006

On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors.

Simon Winwood, Gerwin Klein, Manuel M. T. Chakravarty

Proceedings of the Logic-Based Program Synthesis and Transformation, 2006

Running the manual: an approach to high-assurance microkernel development.

Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty

Proceedings of the ACM SIGPLAN Workshop on Haskell, 2006

Formalising the L4 microkernel API.

Rafal Kolanski, Gerwin Klein

Proceedings of the Theory of Computing 2006, 2006

2005

Verified Java Bytecode Verification (Verified Java Bytecode Verification).

Gerwin Klein

it Inf. Technol., 2005

Jinja is not Java.

Gerwin Klein, Tobias Nipkow

Arch. Formal Proofs, 2005

A Unified Memory Model for Pointers.

Harvey Tuch, Gerwin Klein

Proceedings of the Logic for Programming, 2005

OS Verification - Now!

Harvey Tuch, Gerwin Klein, Gernot Heiser

Proceedings of HotOS'05: 10th Workshop on Hot Topics in Operating Systems, 2005

2004

Verified bytecode verification and type-certifying compilation.

Gerwin Klein, Martin Strecker

J. Log. Algebraic Methods Program., 2004

Example Submission.

Gerwin Klein

Arch. Formal Proofs, 2004

Prototyping Proof Carrying Code.

Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz

Proceedings of the Exploring New Frontiers of Theoretical Informatics, 2004

2003

Verified Java bytecode verification.

Gerwin Klein

PhD thesis, 2003

Verified bytecode verifiers.

Gerwin Klein, Tobias Nipkow

Theor. Comput. Sci., 2003

Verified Bytecode Subroutines.

Gerwin Klein, Martin Wildmoser

J. Autom. Reason., 2003

Verified Java Bytecode Verification.

Gerwin Klein

Proceedings of the Ausgezeichnete Informatikdissertationen 2003, 2003

2001

Verified lightweight bytecode verification.

Gerwin Klein, Tobias Nipkow

Concurr. Comput. Pract. Exp., 2001

1999

FormGen: A Generator for Adaptive Forms Based on EasyGUI.

Alfons Brandl, Gerwin Klein

Proceedings of the Human-Computer Interaction: Ergonomics and User Interfaces, 1999