default search action
Gerwin Klein
Person information
- affiliation: University of New South Wales, Sydney, Australia
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j30]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, Simon Wimmer:
AutoCorres2. Arch. Formal Proofs 2024 (2024) - 2023
- [c56]Robert Sison
, Scott Buckley
Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems. FM 2023: 103-121 - [i4]Scott Buckley, Robert Sison
Proving the Absence of Microarchitectural Timing Channels. CoRR abs/2310.17046 (2023) - 2022
- [j29]Darren D. Cofer
Cyberassured Systems Engineering at Scale. IEEE Secur. Priv. 20(3): 52-64 (2022) - [c55]Zilin Chen, Christine Rizkallah
Property-Based Testing: Climbing the Stairway to Verification. SLE 2022: 84-97 - 2021
- [j28]Liam O'Connor
Cogent: uniqueness types and certifying compilation. J. Funct. Program. 31: e25 (2021) - 2020
- [j27]Gernot Heiser, Gerwin Klein, June Andronick:
seL4 in Australia: from research to real-world trustworthy systems. Commun. ACM 63(4): 72-75 (2020) - [j26]Hira Taqdees Syeda
Formal Reasoning Under Cached Address Translation. J. Autom. Reason. 64(5): 911-945 (2020) - [j25]Gernot Heiser, Toby Murray, Gerwin Klein:
Towards Provable Timing-Channel Prevention. ACM SIGOPS Oper. Syst. Rev. 54(1): 1-7 (2020)
2010 – 2019
- 2019
- [c54]Gernot Heiser, Gerwin Klein, Toby C. Murray:
Can We Prove Time Protection? HotOS 2019: 23-29 - [i3]Gernot Heiser, Gerwin Klein, Toby C. Murray:
Can We Prove Time Protection? CoRR abs/1901.08338 (2019) - 2018
- [j24]Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby C. Murray, Gernot Heiser:
Formally verified software in the real world. Commun. ACM 61(10): 68-77 (2018) - [j23]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): 14-23 (2018) - [j22]Jeremy Avigad
Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. 61(1-4): 1-8 (2018) - [c53]Liam O'Connor
Bringing Effortless Refinement of Data Layouts to Cogent. ISoLA (1) 2018: 134-149 - [c52]Callum Bannister, Peter Höfner, Gerwin Klein:
Backwards and Forwards with Separation Logic. ITP 2018: 68-87 - [c51]Hira Taqdees Syeda
Program Verification in the Presence of Cached Address Translation. ITP 2018: 542-559 - 2017
- [c50]Hira Taqdees Syeda
Reasoning about Translation Lookaside Buffers. LPAR 2017: 490-508 - [c49]Zilin Chen
The Cogent Case for Property-Based Testing. PLOS@SOSP 2017: 1-7 - 2016
- [j21]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) - [j20]Gerwin Klein
Interactive Theorem Proving - Preface of the Special Issue. J. Autom. Reason. 56(3): 201-203 (2016) - [c48]Sidney Amani, Alex Hixon, Zilin Chen
CoGENT: Verifying High-Assurance File System Implementations. ASPLOS 2016: 175-188 - [c47]Liam O'Connor
Refinement through restraint: bringing down the cost of verification. ICFP 2016: 89-102 - [c46]Christine Rizkallah
A Framework for the Automatic Formal Verification of Refinement from Cogent to C. ITP 2016: 323-340 - [i2]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 abs/1601.05520 (2016) - 2015
- [j19]D. Ross Jeffery, Mark Staples, June Andronick, Gerwin Klein
An empirical research agenda for understanding formal methods productivity. Inf. Softw. Technol. 60: 102-112 (2015) - [c45]Matthew Fernandez, June Andronick, Gerwin Klein
Automated Verification of RPC Stub Code. FM 2015: 273-290 - [c44]Daniel Matichuk, Toby C. Murray, June Andronick, D. Ross Jeffery, Gerwin Klein
Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. ICSE (1) 2015: 722-732 - [i1]Darren D. Cofer, Gerwin Klein, Konrad Slind, Virginie Wiels:
Qualification of Formal Methods Tools (Dagstuhl Seminar 15182). Dagstuhl Reports 5(4): 142-159 (2015) - 2014
- [b2]Tobias Nipkow, Gerwin Klein
Concrete Semantics - With Isabelle/HOL. Springer 2014, ISBN 978-3-319-10541-3, pp. 1-280 - [j18]Matthias Daum, Nelson Billing, Gerwin Klein
Concerned with the unprivileged: user programs in kernel refinement. Formal Aspects Comput. 26(6): 1205-1229 (2014) - [j17]Gabriele Keller
File systems deserve verification too! ACM SIGOPS Oper. Syst. Rev. 48(1): 58-64 (2014) - [j16]Gerwin Klein
Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1): 2:1-2:70 (2014) - [c43]Mark Staples, D. Ross Jeffery, June Andronick, Toby C. Murray, Gerwin Klein
Productivity for proof engineering. ESEM 2014: 15:1-15:4 - [c42]Gerwin Klein
Proof Engineering Considered Essential. FM 2014: 16-21 - [c41]David Greenaway, Japheth Lim, June Andronick, Gerwin Klein
Don't sweat the small stuff: formal verification of C code without the pain. PLDI 2014: 429-439 - [p4]Gerwin Klein, Tobias Nipkow:
Applications of Interactive Proof to Data Flow Analysis and Security. Software Systems Safety 2014: 77-134 - [e6]Gerwin Klein, Ruben Gamboa:
Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings. Lecture Notes in Computer Science 8558, Springer 2014, ISBN 978-3-319-08969-0 [contents] - 2013
- [c40]Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein
Formally Verified System Initialisation. ICFEM 2013: 70-85 - [c39]Mark Staples, Rafal Kolanski, Gerwin Klein
Formal specifications better than function points for code sizing. ICSE 2013: 1257-1260 - [c38]Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein
Translation validation for a verified OS kernel. PLDI 2013: 471-482 - [c37]Gabriele Keller
File systems deserve verification too! PLOS@SOSP 2013: 1:1-1:7 - [c36]Matthew Fernandez, Ihor Kuz, Gerwin Klein
Towards a verified component platform. PLOS@SOSP 2013: 2:1-2:7 - [c35]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: 415-429 - 2012
- [j15]Gerwin Klein, Rafal Kolanski, Andrew Boyton:
Separation Algebra. Arch. Formal Proofs 2012 (2012) - [j14]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): 115- (2012) - [j13]Gernot Heiser, Toby C. Murray, Gerwin Klein
It's Time for Trustworthy Systems. IEEE Secur. Priv. 10(2): 67-70 (2012) - [c34]Timothy Bourke, Matthias Daum, Gerwin Klein
Challenges and Experiences in Managing Large-Scale Proofs. AISC/MKM/Calculemus 2012: 32-48 - [c33]Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein
Noninterference for Operating System Kernels. CPP 2012: 126-142 - [c32]June Andronick, D. Ross Jeffery, Gerwin Klein
Large-scale formal verification in practice: A process perspective. ICSE 2012: 1002-1011 - [c31]He Zhang, Gerwin Klein
Simulation modeling of a large-scale formal verification process. ICSSP 2012: 3-12 - [c30]David Greenaway, June Andronick, Gerwin Klein
Bridging the Gap: Automatic Verified Abstraction of C. ITP 2012: 99-115 - [c29]Gerwin Klein
Mechanised Separation Algebra. ITP 2012: 332-337 - [p3]Gerwin Klein:
Interactive Proof: Applications to Semantics. Software Safety and Security 2012: 85-125 - [e5]Franck Cassez, Ralf Huuck, Gerwin Klein, Bastian Schlich:
Proceedings Seventh Conference on Systems Software Verification, SSV 2012, Sydney, Australia, 28-30 November 2012. EPTCS 102, 2012 [contents] - 2011
- [c28]Gerwin Klein, Toby C. Murray, Peter Gammie, Thomas Sewell, Simon Winwood:
Provable Security: How Feasible Is It? HotOS 2011 - [c27]Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein
seL4 Enforces Integrity. ITP 2011: 325-340 - 2010
- [j12]Gerwin Klein
seL4: formal verification of an operating-system kernel. Commun. ACM 53(6): 107-115 (2010) - [c26]Gerwin Klein
From a Verified Kernel towards Verified Systems. APLAS 2010: 21-33 - [c25]Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz, Leonid Ryzhyk:
The road to trustworthy systems. STC@CCS 2010: 3-10 - [c24]Gerwin Klein
A Formally Verified OS Kernel. Now What? ITP 2010: 1-7 - [c23]Ihor Kuz, Gerwin Klein
capDL: a language for describing capability-based systems. ApSys 2010: 31-36 - [c22]Gerwin Klein
The L4.verified Project - Next Steps. VSTTE 2010: 86-96 - [p2]Gerwin Klein
Refinement in the Formal Verification of the seL4 Microkernel. Design and Verification of Microprocessor Systems for High-Assurance Applications 2010: 323-339 - [e4]Ralf Huuck, Gerwin Klein, Bastian Schlich:
5th International Workshop on Systems Software Verification, SSV'10, Vancouver, BC, Canada, October 6-7, 2010. USENIX Association 2010 [contents]
2000 – 2009
- 2009
- [j11]Gerwin Klein
Operating System Verification. J. Autom. Reason. 42(2-4): 123-124 (2009) - [j10]Gerwin Klein:
Correct OS Kernel? Proof? Done! login Usenix Mag. 34(6) (2009) - [c21]Gerwin Klein
Experience report: seL4: formally verifying a high-performance microkernel. ICFP 2009: 91-96 - [c20]Gerwin Klein
seL4: formal verification of an OS kernel. SOSP 2009: 207-220 - [c19]Rafal Kolanski, Gerwin Klein
Types, Maps and Separation Logic. TPHOLs 2009: 276-292 - [c18]Simon Winwood, Gerwin Klein
Mind the Gap. TPHOLs 2009: 500-515 - [c17]Ralf Huuck, Gerwin Klein, Bastian Schlich:
Preface. SSV 2009: 1-3 - 2008
- [c16]Bernhard Beckert, Gerwin Klein:
Title, Preface, Table of Contents. VERIFY 2008 - [c15]David A. Cock
Secure Microkernels, State Monads and Scalable Refinement. TPHOLs 2008: 167-182 - [c14]Rafal Kolanski, Gerwin Klein:
Mapped Separation Logic. VSTTE 2008: 15-29 - [c13]Dhammika Elkaduwe, Gerwin Klein
Verified Protection Model of the seL4 Microkernel. VSTTE 2008: 99-114 - [c12]Ralf Huuck, Gerwin Klein, Bastian Schlich:
Preface. SSV 2008: 1-3 - [e3]Bernhard Beckert, Gerwin Klein:
Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, Sydney, Australia, August 10-11, 2008. CEUR Workshop Proceedings 372, CEUR-WS.org 2008 [contents] - [e2]Ralf Huuck, Gerwin Klein, Bastian Schlich:
Proceedings of the 3rd International Workshop on Systems Software Verification, SSV 2008, Sydney, Australia, February 25-27, 2008. Electronic Notes in Theoretical Computer Science 217, Elsevier 2008 [contents] - [e1]Ralf Huuck, Gerwin Klein, Bastian Schlich:
Proceedings of the 4th International Workshop on Systems Software Verification, SSV 2009, Aachen, Germany, June 22-24, 2009. Electronic Notes in Theoretical Computer Science 254, Elsevier 2008 [contents] - 2007
- [j9]Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein
Towards trustworthy computing systems: taking microkernels to the next level. ACM SIGOPS Oper. Syst. Rev. 41(4): 3-11 (2007) - [c11]Jia Meng, Lawrence C. Paulson, Gerwin Klein:
A Termination Checker for Isabelle Hoare Logic. VERIFY 2007 - [c10]Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe, Gernot Heiser:
Towards a Practical, Verified Kernel. HotOS 2007 - [c9]Harvey Tuch, Gerwin Klein
Types, bytes, and separation logic. POPL 2007: 97-108 - 2006
- [j8]Gerwin Klein
A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4): 619-695 (2006) - [c8]Rafal Kolanski, Gerwin Klein:
Formalising the L4 microkernel API. CATS 2006: 53-68 - [c7]Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty:
Running the manual: an approach to high-assurance microkernel development. Haskell 2006: 60-71 - [c6]Simon Winwood, Gerwin Klein
On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors. LOPSTR 2006: 111-126 - 2005
- [j7]Gerwin Klein, Tobias Nipkow:
Jinja is not Java. Arch. Formal Proofs 2005 (2005) - [j6]Gerwin Klein
Verified Java Bytecode Verification (Verified Java Bytecode Verification). it Inf. Technol. 47(2): 107-110 (2005) - [c5]Harvey Tuch, Gerwin Klein, Gernot Heiser:
OS Verification - Now! HotOS 2005 - [c4]Harvey Tuch, Gerwin Klein
A Unified Memory Model for Pointers. LPAR 2005: 474-488 - 2004
- [j5]Gerwin Klein:
Example Submission. Arch. Formal Proofs 2004 (2004) - [j4]Gerwin Klein
Verified bytecode verification and type-certifying compilation. J. Log. Algebraic Methods Program. 58(1-2): 27-60 (2004) - [c3]Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz:
Prototyping Proof Carrying Code. IFIP TCS 2004: 333-347 - 2003
- [b1]Gerwin Klein:
Verified Java bytecode verification. Technical University Munich, Germany, 2003 - [j3]Gerwin Klein
Verified Bytecode Subroutines. J. Autom. Reason. 30(3-4): 363-398 (2003) - [j2]Gerwin Klein
Verified bytecode verifiers. Theor. Comput. Sci. 298(3): 583-626 (2003) - [c2]Gerwin Klein, Martin Wildmoser:
Verified Bytecode Subroutines. TPHOLs 2003: 55-70 - [p1]Gerwin Klein:
Verified Java Bytecode Verification. Ausgezeichnete Informatikdissertationen 2003: 91-100 - 2001
- [j1]Gerwin Klein
Verified lightweight bytecode verification. Concurr. Comput. Pract. Exp. 13(13): 1133-1151 (2001)
1990 – 1999
- 1999
- [c1]Alfons Brandl, Gerwin Klein:
FormGen: A Generator for Adaptive Forms Based on EasyGUI. HCI (1) 1999: 1172-1176
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-05 21:17 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: