Gerwin Klein

ORCID

Publication Activity (10 Years)

Years Active: 1999-2023
Publications (10 Years): 28

Top Venues

ITP

CoRR

J. Autom. Reason.

Technical University Munich, Germany (PHD)

Education History

Technical University Munich, Germany

PHD

Publications

Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein, Gernot Heiser
Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems. FM (2023)
Scott Buckley, Robert Sison, Nils Wistoff, Curtis Millar, Toby Murray, Gerwin Klein, Gernot Heiser
Proving the Absence of Microarchitectural Timing Channels. CoRR (2023)
Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser, Gabriele Keller
Property-Based Testing: Climbing the Stairway to Verification. SLE (2022)
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
Cyberassured Systems Engineering at Scale. IEEE Secur. Priv. 20 (3) (2022)
Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, Gabriele Keller
Cogent: uniqueness types and certifying compilation. J. Funct. Program. 31 (2021)
Hira Taqdees Syeda, Gerwin Klein
Formal Reasoning Under Cached Address Translation. J. Autom. Reason. 64 (5) (2020)
Gernot Heiser, Toby Murray, Gerwin Klein
Towards Provable Timing-Channel Prevention. ACM SIGOPS Oper. Syst. Rev. 54 (1) (2020)
Gernot Heiser, Gerwin Klein, June Andronick
seL4 in Australia: from research to real-world trustworthy systems. Commun. ACM 63 (4) (2020)
Gernot Heiser, Gerwin Klein, Toby C. Murray
Can We Prove Time Protection? HotOS (2019)
Gernot Heiser, Gerwin Klein, Toby C. Murray
Can We Prove Time Protection? CoRR (2019)
Hira Taqdees Syeda, Gerwin Klein
Program Verification in the Presence of Cached Address Translation. ITP (2018)
Liam O'Connor, Zilin Chen, Partha Susarla, Christine Rizkallah, Gerwin Klein, Gabriele Keller
Bringing Effortless Refinement of Data Layouts to Cogent. ISoLA (1) (2018)
Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby C. Murray, Gernot Heiser
Formally verified software in the real world. Commun. ACM 61 (10) (2018)
Callum Bannister, Peter Höfner, Gerwin Klein
Backwards and Forwards with Separation Logic. ITP (2018)
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
A Formal Approach to Constructing Secure Air Vehicle Software. Computer 51 (11) (2018)
Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting
Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. 61 (1-4) (2018)
Hira Taqdees Syeda, Gerwin Klein
Reasoning about Translation Lookaside Buffers. LPAR (2017)
Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein, Gernot Heiser
The Cogent Case for Property-Based Testing. PLOS@SOSP (2017)
Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein
A Framework for the Automatic Formal Verification of Refinement from Cogent to C. ITP (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 C. Murray, Gerwin Klein, Gernot Heiser
CoGENT: Verifying High-Assurance File System Implementations. ASPLOS (2016)
Gerwin Klein, Ruben Gamboa
Interactive Theorem Proving - Preface of the Special Issue. J. Autom. Reason. 56 (3) (2016)
Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, Gerwin Klein
COGENT: Certified Compilation for a Functional Systems Language. CoRR (2016)
Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby C. Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein
Refinement through restraint: bringing down the cost of verification. ICFP (2016)
Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk, Thomas Sewell
Finite Machine Word Library. Arch. Formal Proofs 2016 (2016)
Matthew Fernandez, June Andronick, Gerwin Klein, Ihor Kuz
Automated Verification of RPC Stub Code. FM (2015)
Darren D. Cofer, Gerwin Klein, Konrad Slind, Virginie Wiels
Qualification of Formal Methods Tools (Dagstuhl Seminar 15182). Dagstuhl Reports 5 (4) (2015)
D. Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein, Toby C. Murray
An empirical research agenda for understanding formal methods productivity. Inf. Softw. Technol. 60 (2015)
Daniel Matichuk, Toby C. Murray, June Andronick, D. Ross Jeffery, Gerwin Klein, Mark Staples
Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. ICSE (1) (2015)
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser
Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32 (1) (2014)
Matthias Daum, Nelson Billing, Gerwin Klein
Concerned with the unprivileged: user programs in kernel refinement. Formal Aspects Comput. 26 (6) (2014)
Mark Staples, D. Ross Jeffery, June Andronick, Toby C. Murray, Gerwin Klein, Rafal Kolanski
Productivity for proof engineering. ESEM (2014)
Gerwin Klein
Proof Engineering Considered Essential. FM (2014)
Gabriele Keller, Toby C. Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, Gernot Heiser
File systems deserve verification too! ACM SIGOPS Oper. Syst. Rev. 48 (1) (2014)
David Greenaway, Japheth Lim, June Andronick, Gerwin Klein
Don't sweat the small stuff: formal verification of C code without the pain. PLDI (2014)
Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, Gerwin Klein
seL4: From General Purpose to a Proof of Information Flow Enforcement. IEEE Symposium on Security and Privacy (2013)
Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein
Translation validation for a verified OS kernel. PLDI (2013)
Mark Staples, Rafal Kolanski, Gerwin Klein, Corey Lewis, June Andronick, Toby C. Murray, D. Ross Jeffery, Len Bass
Formal specifications better than function points for code sizing. ICSE (2013)
Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis, Thomas Sewell
Formally Verified System Initialisation. ICFEM (2013)
Matthew Fernandez, Ihor Kuz, Gerwin Klein, June Andronick
Towards a verified component platform. PLOS@SOSP (2013)
Gabriele Keller, Toby C. Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, Gernot Heiser
File systems deserve verification too! PLOS@SOSP (2013)
He Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu, Rafal Kolanski
Simulation modeling of a large-scale formal verification process. ICSSP (2012)
Gerwin Klein, Rafal Kolanski, Andrew Boyton
Mechanised Separation Algebra. ITP (2012)
Gernot Heiser, Toby C. Murray, Gerwin Klein
It's Time for Trustworthy Systems. IEEE Secur. Priv. 10 (2) (2012)
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@NICTA. AI Mag. 33 (3) (2012)
David Greenaway, June Andronick, Gerwin Klein
Bridging the Gap: Automatic Verified Abstraction of C. ITP (2012)
Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein
Noninterference for Operating System Kernels. CPP (2012)
Timothy Bourke, Matthias Daum, Gerwin Klein, Rafal Kolanski
Challenges and Experiences in Managing Large-Scale Proofs. AISC/MKM/Calculemus (2012)
Gerwin Klein, Rafal Kolanski, Andrew Boyton
Separation Algebra. Arch. Formal Proofs 2012 (2012)
June Andronick, D. Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He Zhang, Liming Zhu
Large-scale formal verification in practice: A process perspective. ICSE (2012)
Gerwin Klein, Toby C. Murray, Peter Gammie, Thomas Sewell, Simon Winwood
Provable Security: How Feasible Is It? HotOS (2011)
Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein
seL4 Enforces Integrity. ITP (2011)
Ihor Kuz, Gerwin Klein, Corey Lewis, Adam Walker
capDL: a language for describing capability-based systems. ApSys (2010)
Gerwin Klein
A Formally Verified OS Kernel. Now What? ITP (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, Simon Winwood
seL4: formal verification of an operating-system kernel. Commun. ACM 53 (6) (2010)
Gerwin Klein
The L4.verified Project - Next Steps. VSTTE (2010)
Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz, Leonid Ryzhyk
The road to trustworthy systems. STC@CCS (2010)
Gerwin Klein
From a Verified Kernel towards Verified Systems. APLAS (2010)
Gerwin Klein, Philip Derrin, Kevin Elphinstone
Experience report: seL4: formally verifying a high-performance microkernel. ICFP (2009)
Ralf Huuck, Gerwin Klein, Bastian Schlich
Preface. Electron. Notes Theor. Comput. Sci. 254 (2009)
Gerwin Klein, Ralf Huuck, Bastian Schlich
Operating System Verification. J. Autom. Reason. 42 (2-4) (2009)
Rafal Kolanski, Gerwin Klein
Types, Maps and Separation Logic. TPHOLs (2009)
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish
Mind the Gap. TPHOLs (2009)
Gerwin Klein
Correct OS Kernel? Proof? Done! login Usenix Mag. 34 (6) (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, Simon Winwood
seL4: formal verification of an OS kernel. SOSP (2009)
Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone
Verified Protection Model of the seL4 Microkernel. VSTTE (2008)
Bernhard Beckert, Gerwin Klein
Title, Preface, Table of Contents. VERIFY (2008)
Rafal Kolanski, Gerwin Klein
Mapped Separation Logic. VSTTE (2008)
David Cock, Gerwin Klein, Thomas Sewell
Secure Microkernels, State Monads and Scalable Refinement. TPHOLs (2008)
Ralf Huuck, Gerwin Klein, Bastian Schlich
Preface. Electron. Notes Theor. Comput. Sci. 217 (2008)
Jia Meng, Lawrence C. Paulson, Gerwin Klein
A Termination Checker for Isabelle Hoare Logic. VERIFY (2007)
Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe, Gernot Heiser
Towards a Practical, Verified Kernel. HotOS (2007)
Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein, Stefan M. Petters
Towards trustworthy computing systems: taking microkernels to the next level. ACM SIGOPS Oper. Syst. Rev. 41 (4) (2007)
Harvey Tuch, Gerwin Klein, Michael Norrish
Types, bytes, and separation logic. POPL (2007)
Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, Manuel M. T. Chakravarty
Running the manual: an approach to high-assurance microkernel development. Haskell (2006)
Rafal Kolanski, Gerwin Klein
Formalising the L4 microkernel API. CATS (2006)
Simon Winwood, Gerwin Klein, Manuel M. T. Chakravarty
On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors. LOPSTR (2006)
Gerwin Klein, Tobias Nipkow
A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28 (4) (2006)
Harvey Tuch, Gerwin Klein, Gernot Heiser
OS Verification - Now! HotOS (2005)
Gerwin Klein, Tobias Nipkow
Jinja is not Java. Arch. Formal Proofs 2005 (2005)
Harvey Tuch, Gerwin Klein
A Unified Memory Model for Pointers. LPAR (2005)
Gerwin Klein
Verified Java Bytecode Verification (Verified Java Bytecode Verification). it Inf. Technol. 47 (2) (2005)
Gerwin Klein, Martin Strecker
Verified bytecode verification and type-certifying compilation. J. Log. Algebraic Methods Program. 58 (1-2) (2004)
Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz
Prototyping Proof Carrying Code. IFIP TCS (2004)
Gerwin Klein
Example Submission. Arch. Formal Proofs 2004 (2004)
Gerwin Klein, Martin Wildmoser
Verified Bytecode Subroutines. TPHOLs (2003)
Gerwin Klein, Tobias Nipkow
Verified bytecode verifiers. Theor. Comput. Sci. 298 (3) (2003)
Gerwin Klein
Verified Java Bytecode Verification. Ausgezeichnete Informatikdissertationen (2003)
Gerwin Klein, Martin Wildmoser
Verified Bytecode Subroutines. J. Autom. Reason. 30 (3-4) (2003)
Gerwin Klein, Tobias Nipkow
Verified lightweight bytecode verification. Concurr. Comput. Pract. Exp. 13 (13) (2001)
Alfons Brandl, Gerwin Klein
FormGen: A Generator for Adaptive Forms Based on EasyGUI. HCI (1) (1999)

Gerwin Klein.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Gerwin Klein