FormGen: A Generator for Adaptive Forms Based on EasyGUI. - Alfons Brandl; Gerwin Klein (HCI (1), 1999)

Verified lightweight bytecode verification. - Gerwin Klein; Tobias Nipkow (Concurr. Comput. Pract. Exp., 2001)

Verified Java Bytecode Verification. - Gerwin Klein (Ausgezeichnete Informatikdissertationen, 2003)

Verified Bytecode Subroutines. - Gerwin Klein; Martin Wildmoser (J. Autom. Reason., 2003)

Verified bytecode verifiers. - Gerwin Klein; Tobias Nipkow (Theor. Comput. Sci., 2003)

Verified Java bytecode verification. - Gerwin Klein (2003)

Prototyping Proof Carrying Code. - Martin Wildmoser; Tobias Nipkow; Gerwin Klein; Sebastian Nanz (IFIP TCS, 2004)

Example Submission. - Gerwin Klein (Arch. Formal Proofs, 2004)

Verified bytecode verification and type-certifying compilation. - Gerwin Klein; Martin Strecker (J. Log. Algebraic Methods Program., 2004)

OS Verification - Now! - Harvey Tuch; Gerwin Klein; Gernot Heiser (HotOS, 2005)

A Unified Memory Model for Pointers. - Harvey Tuch; Gerwin Klein (LPAR, 2005)

Jinja is not Java. - Gerwin Klein; Tobias Nipkow (Arch. Formal Proofs, 2005)

Verified Java Bytecode Verification (Verified Java Bytecode Verification). - Gerwin Klein (it Inf. Technol., 2005)

Formalising the L4 microkernel API. - Rafal Kolanski; Gerwin Klein (CATS, 2006)

Running the manual: an approach to high-assurance microkernel development. - Philip Derrin; Kevin Elphinstone; Gerwin Klein; David A. Cock; Manuel M. T. Chakravarty (Haskell, 2006)

On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors. - Simon Winwood; Gerwin Klein; Manuel M. T. Chakravarty (LOPSTR, 2006)

A machine-checked model for a Java-like language, virtual machine, and compiler. - Gerwin Klein; Tobias Nipkow (ACM Trans. Program. Lang. Syst., 2006)

A Termination Checker for Isabelle Hoare Logic. - Jia Meng 002; Lawrence C. Paulson; Gerwin Klein (VERIFY, 2007)

Towards a Practical, Verified Kernel. - Kevin Elphinstone; Gerwin Klein; Philip Derrin; Timothy Roscoe; Gernot Heiser (HotOS, 2007)

Types, bytes, and separation logic. - Harvey Tuch; Gerwin Klein; Michael Norrish (POPL, 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)

Title, Preface, Table of Contents. - Bernhard Beckert; Gerwin Klein (VERIFY, 2008)

Secure Microkernels, State Monads and Scalable Refinement. - David A. Cock; Gerwin Klein; Thomas Sewell (TPHOLs, 2008)

Verified Protection Model of the seL4 Microkernel. - Dhammika Elkaduwe; Gerwin Klein; Kevin Elphinstone (VSTTE, 2008)

Mapped Separation Logic. - Rafal Kolanski; Gerwin Klein (VSTTE, 2008)

Experience report: seL4: formally verifying a high-performance microkernel. - Gerwin Klein; Philip Derrin; Kevin Elphinstone (ICFP, 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; et al. (SOSP, 2009)

Types, Maps and Separation Logic. - Rafal Kolanski; Gerwin Klein (TPHOLs, 2009)

Mind the Gap. - Simon Winwood; Gerwin Klein; Thomas Sewell; June Andronick; David A. Cock; Michael Norrish (TPHOLs, 2009)

Preface. - Ralf Huuck; Gerwin Klein; Bastian Schlich (SSV, 2009)

Operating System Verification. - Gerwin Klein; Ralf Huuck; Bastian Schlich (J. Autom. Reason., 2009)

Correct OS Kernel? Proof? Done! - Gerwin Klein (login Usenix Mag., 2009)

Refinement in the Formal Verification of the seL4 Microkernel. - Gerwin Klein; Thomas Sewell; Simon Winwood (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

From a Verified Kernel towards Verified Systems. - Gerwin Klein (APLAS, 2010)

The road to trustworthy systems. - Gernot Heiser; June Andronick; Kevin Elphinstone; Gerwin Klein; Ihor Kuz; Leonid Ryzhyk (STC@CCS, 2010)

A Formally Verified OS Kernel. Now What? - Gerwin Klein (ITP, 2010)

capDL: a language for describing capability-based systems. - Ihor Kuz; Gerwin Klein; Corey Lewis; Adam Walker (ApSys, 2010)

The L4.verified Project - Next Steps. - Gerwin Klein (VSTTE, 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; et al. (Commun. ACM, 2010)

Provable Security: How Feasible Is It? - Gerwin Klein; Toby C. Murray; Peter Gammie; Thomas Sewell; Simon Winwood (HotOS, 2011)

seL4 Enforces Integrity. - Thomas Sewell; Simon Winwood; Peter Gammie; Toby C. Murray; June Andronick; Gerwin Klein (ITP, 2011)

Challenges and Experiences in Managing Large-Scale Proofs. - Timothy Bourke; Matthias Daum 001; Gerwin Klein; Rafal Kolanski (AISC/MKM/Calculemus, 2012)

Noninterference for Operating System Kernels. - Toby C. Murray; Daniel Matichuk; Matthew Brassil; Peter Gammie; Gerwin Klein (CPP, 2012)

Large-scale formal verification in practice: A process perspective. - June Andronick; D. Ross Jeffery; Gerwin Klein; Rafal Kolanski; Mark Staples; He Zhang 001; Liming Zhu 001 (ICSE, 2012)

Simulation modeling of a large-scale formal verification process. - He Zhang 001; Gerwin Klein; Mark Staples; June Andronick; Liming Zhu 001; Rafal Kolanski (ICSSP, 2012)

Bridging the Gap: Automatic Verified Abstraction of C. - David Greenaway; June Andronick; Gerwin Klein (ITP, 2012)

Mechanised Separation Algebra. - Gerwin Klein; Rafal Kolanski; Andrew Boyton (ITP, 2012)

Separation Algebra. - Gerwin Klein; Rafal Kolanski; Andrew Boyton (Arch. Formal Proofs, 2012)

AI@NICTA. - Nick Barnes; Peter Baumgartner 001; Tibério S. Caetano; Hugh F. Durrant-Whyte; Gerwin Klein; Penelope Sanderson; Abdul Sattar 001; Peter J. Stuckey; Sylvie Thiébaux; Pascal Van Hentenryck; Toby Walsh (AI Mag., 2012)

It's Time for Trustworthy Systems. - Gernot Heiser; Toby C. Murray; Gerwin Klein (IEEE Secur. Priv., 2012)

Interactive Proof: Applications to Semantics. - Gerwin Klein (Software Safety and Security, 2012)

Formally Verified System Initialisation. - Andrew Boyton; June Andronick; Callum Bannister; Matthew Fernandez; Xin Gao; David Greenaway; Gerwin Klein; Corey Lewis; Thomas Sewell (ICFEM, 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 (ICSE, 2013)

Translation validation for a verified OS kernel. - Thomas Arthur Leck Sewell; Magnus O. Myreen; Gerwin Klein (PLDI, 2013)

Towards a verified component platform. - Matthew Fernandez; Ihor Kuz; Gerwin Klein; June Andronick (PLOS@SOSP, 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 (IEEE Symposium on Security and Privacy, 2013)

Concrete Semantics - With Isabelle/HOL - Tobias Nipkow; Gerwin Klein (Springer, 2014)

Productivity for proof engineering. - Mark Staples; D. Ross Jeffery; June Andronick; Toby C. Murray; Gerwin Klein; Rafal Kolanski (ESEM, 2014)

Proof Engineering Considered Essential. - Gerwin Klein (FM, 2014)

Don't sweat the small stuff: formal verification of C code without the pain. - David Greenaway; Japheth Lim; June Andronick; Gerwin Klein (PLDI, 2014)

Concerned with the unprivileged: user programs in kernel refinement. - Matthias Daum 001; Nelson Billing; Gerwin Klein (Formal Aspects Comput., 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)

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)

Applications of Interactive Proof to Data Flow Analysis and Security. - Gerwin Klein; Tobias Nipkow (Software Systems Safety, 2014)

Automated Verification of RPC Stub Code. - Matthew Fernandez; June Andronick; Gerwin Klein; Ihor Kuz (FM, 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 (ICSE (1), 2015)

Qualification of Formal Methods Tools (Dagstuhl Seminar 15182). - Darren D. Cofer; Gerwin Klein; Konrad Slind; Virginie Wiels (Dagstuhl Reports, 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)

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; et al. (ASPLOS, 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 (ICFP, 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 (ITP, 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)

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)

Interactive Theorem Proving - Preface of the Special Issue. - Gerwin Klein; Ruben Gamboa (J. Autom. Reason., 2016)

Reasoning about Translation Lookaside Buffers. - Hira Taqdees Syeda; Gerwin Klein (LPAR, 2017)

The Cogent Case for Property-Based Testing. - Zilin Chen; Liam O'Connor; Gabriele Keller; Gerwin Klein; Gernot Heiser (PLOS@SOSP, 2017)

Bringing Effortless Refinement of Data Layouts to Cogent. - Liam O'Connor; Zilin Chen; Partha Susarla; Christine Rizkallah; Gerwin Klein; Gabriele Keller (ISoLA (1), 2018)

Backwards and Forwards with Separation Logic. - Callum Bannister; Peter Höfner; Gerwin Klein (ITP, 2018)

Program Verification in the Presence of Cached Address Translation. - Hira Taqdees Syeda; Gerwin Klein (ITP, 2018)

Formally verified software in the real world. - Gerwin Klein; June Andronick; Matthew Fernandez; Ihor Kuz; Toby C. Murray; Gernot Heiser (Commun. ACM, 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)

Introduction to Milestones in Interactive Theorem Proving. - Jeremy Avigad; Jasmin Christian Blanchette; Gerwin Klein; Lawrence C. Paulson; Andrei Popescu 001; Gregor Snelting (J. Autom. Reason., 2018)

Can We Prove Time Protection? - Gernot Heiser; Gerwin Klein; Toby C. Murray (HotOS, 2019)

seL4 in Australia: from research to real-world trustworthy systems. - Gernot Heiser; Gerwin Klein; June Andronick (Commun. ACM, 2020)

Formal Reasoning Under Cached Address Translation. - Hira Taqdees Syeda; Gerwin Klein (J. Autom. Reason., 2020)

Towards Provable Timing-Channel Prevention. - Gernot Heiser; Toby Murray; Gerwin Klein (ACM SIGOPS Oper. Syst. Rev., 2020)

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)

Property-Based Testing: Climbing the Stairway to Verification. - Zilin Chen; Christine Rizkallah; Liam O'Connor; Partha Susarla; Gerwin Klein; Gernot Heiser; Gabriele Keller (SLE, 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)

Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems. - Robert Sison; Scott Buckley; Toby Murray; Gerwin Klein; Gernot Heiser (FM, 2023)

Proving the Absence of Microarchitectural Timing Channels. - Scott Buckley; Robert Sison; Nils Wistoff; Curtis Millar; Toby Murray; Gerwin Klein; Gernot Heiser (CoRR, 2023)

AutoCorres2. - Matthew Brecknell; David Greenaway; Johannes Hölzl; Fabian Immler; Gerwin Klein; Rafal Kolanski; Japheth Lim; Michael Norrish; Norbert Schirmer; Salomon Sickert; Thomas Sewell; Harvey Tuch; et al. (Arch. Formal Proofs, 2024)