Gerwin Klein
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
46
Venues
26
Active years
1999–2026
Best venue rank
A*
Where they publish
- BITP7 papers
- AHotOS4 papers
- A*SOSP4 papers
- BFM3 papers
- A*ICSE3 papers
- BLPAR2 papers
- AICFP2 papers
- A*PLDI2 papers
- ACADE2 papers
- A*LICS1 paper
- CICTAC1 paper
- BSLE1 paper
- CISoLA1 paper
- A*ASPLOS1 paper
- AESEM1 paper
- CICFEM1 paper
- A*SP1 paper
- AustralasianAISC1 paper
- BCPP1 paper
- BAPLAS1 paper
- A*CCS1 paper
- A*SIGCOMM1 paper
- A*POPL1 paper
- CHASKELL1 paper
- CLOPSTR1 paper
- NationalHCI1 paper
Papers
46 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | LICS | The Algebra of Iterative Constructions. | Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Todd Schmid, Henning Urbat |
| 2025 | ICTAC | A Rely-Guarantee-Based Simulation for Cooperative Semantics. | Kevin Tran, Johannes man Pohjola, Rob Sison, Gerwin Klein |
| 2023 | FM | Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems. | Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein, Gernot Heiser |
| 2022 | SLE | Property-Based Testing: Climbing the Stairway to Verification. | Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser, Gabriele Keller |
| 2019 | HotOS | Can We Prove Time Protection? | Gernot Heiser, Gerwin Klein, Toby C. Murray |
| 2018 | ISoLA | Bringing Effortless Refinement of Data Layouts to Cogent. | Liam O'Connor, Zilin Chen, Partha Susarla, Christine Rizkallah, Gerwin Klein, Gabriele Keller |
| 2018 | ITP | Backwards and Forwards with Separation Logic. | Callum Bannister, Peter Hfner, Gerwin Klein |
| 2018 | ITP | Program Verification in the Presence of Cached Address Translation. | Hira Taqdees Syeda, Gerwin Klein |
| 2017 | LPAR | Reasoning about Translation Lookaside Buffers. | Hira Taqdees Syeda, Gerwin Klein |
| 2017 | SOSP | The Cogent Case for Property-Based Testing. | Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein, Gernot Heiser |
| 2016 | ASPLOS | 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 |
| 2016 | ICFP | 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 |
| 2016 | ITP | 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 |
| 2015 | FM | Automated Verification of RPC Stub Code. | Matthew Fernandez, June Andronick, Gerwin Klein, Ihor Kuz |
| 2015 | ICSE | 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 |
| 2014 | ESEM | Productivity for proof engineering. | Mark Staples, D. Ross Jeffery, June Andronick, Toby C. Murray, Gerwin Klein, Rafal Kolanski |
| 2014 | FM | Proof Engineering Considered Essential. | Gerwin Klein |
| 2014 | PLDI | Don't sweat the small stuff: formal verification of C code without the pain. | David Greenaway, Japheth Lim, June Andronick, Gerwin Klein |
| 2013 | ICFEM | Formally Verified System Initialisation. | Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis, Thomas Sewell |
| 2013 | ICSE | 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 |
| 2013 | PLDI | Translation validation for a verified OS kernel. | Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein |
| 2013 | SP | 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 |
| 2013 | SOSP | Towards a verified component platform. | Matthew Fernandez, Ihor Kuz, Gerwin Klein, June Andronick |
| 2013 | SOSP | File systems deserve verification too! | Gabriele Keller, Toby C. Murray, Sidney Amani, Liam O'Connor, Zilin Chen, Leonid Ryzhyk, Gerwin Klein, Gernot Heiser |
| 2012 | AISC | Challenges and Experiences in Managing Large-Scale Proofs. | Timothy Bourke, Matthias Daum, Gerwin Klein, Rafal Kolanski |
| 2012 | CPP | Noninterference for Operating System Kernels. | Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein |
| 2012 | ICSE | Large-scale formal verification in practice: A process perspective. | June Andronick, D. Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He Zhang, Liming Zhu |
| 2012 | ITP | Bridging the Gap: Automatic Verified Abstraction of C. | David Greenaway, June Andronick, Gerwin Klein |
| 2012 | ITP | Mechanised Separation Algebra. | Gerwin Klein, Rafal Kolanski, Andrew Boyton |
| 2011 | HotOS | Provable Security: How Feasible Is It? | Gerwin Klein, Toby C. Murray, Peter Gammie, Thomas Sewell, Simon Winwood |
| 2011 | ITP | seL4 Enforces Integrity. | Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein |
| 2010 | APLAS | From a Verified Kernel towards Verified Systems. | Gerwin Klein |
| 2010 | CCS | The road to trustworthy systems. | Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz, Leonid Ryzhyk |
| 2010 | ITP | A Formally Verified OS Kernel. Now What? | Gerwin Klein |
| 2010 | SIGCOMM | capDL: a language for describing capability-based systems. | Ihor Kuz, Gerwin Klein, Corey Lewis, Adam Walker |
| 2009 | ICFP | Experience report: seL4: formally verifying a high-performance microkernel. | Gerwin Klein, Philip Derrin, Kevin Elphinstone |
| 2009 | SOSP | 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 |
| 2008 | CADE | Title, Preface, Table of Contents. | Bernhard Beckert, Gerwin Klein |
| 2007 | CADE | A Termination Checker for Isabelle Hoare Logic. | Jia Meng, Lawrence C. Paulson, Gerwin Klein |
| 2007 | HotOS | Towards a Practical, Verified Kernel. | Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe, Gernot Heiser |
| 2007 | POPL | Types, bytes, and separation logic. | Harvey Tuch, Gerwin Klein, Michael Norrish |
| 2006 | HASKELL | Running the manual: an approach to high-assurance microkernel development. | Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty |
| 2006 | LOPSTR | On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors. | Simon Winwood, Gerwin Klein, Manuel M. T. Chakravarty |
| 2005 | HotOS | OS Verification - Now! | Harvey Tuch, Gerwin Klein, Gernot Heiser |
| 2005 | LPAR | A Unified Memory Model for Pointers. | Harvey Tuch, Gerwin Klein |
| 1999 | HCI | FormGen: A Generator for Adaptive Forms Based on EasyGUI. | Alfons Brandl, Gerwin Klein |