Please note: This is a beta version of the new dblp website.
You can find the classic dblp view of this page here.
You can find the classic dblp view of this page here.
Gerwin Klein
2010 – today
- 2013
[c33]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: 1257-1260
[c32]Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein: Translation validation for a verified OS kernel. PLDI 2013: 471-482
[c31]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
[j16]Gerwin Klein, Rafal Kolanski, Andrew Boyton: Separation Algebra. Archive of Formal Proofs 2012 (2012)
[j15]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 Magazine 33(3): 115- (2012)
[j14]Gernot Heiser, Toby C. Murray, Gerwin Klein: It's Time for Trustworthy Systems. IEEE Security & Privacy 10(2): 67-70 (2012)
[c30]Timothy Bourke, Matthias Daum, Gerwin Klein, Rafal Kolanski: Challenges and Experiences in Managing Large-Scale Proofs. AISC/MKM/Calculemus 2012: 32-48
[c29]Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein: Noninterference for Operating System Kernels. CPP 2012: 126-142
[c28]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: 1002-1011
[c27]He Zhang, Gerwin Klein, Mark Staples, June Andronick, Liming Zhu, Rafal Kolanski: Simulation modeling of a large-scale formal verification process. ICSSP 2012: 3-12
[c26]David Greenaway, June Andronick, Gerwin Klein: Bridging the Gap: Automatic Verified Abstraction of C. ITP 2012: 99-115
[c25]
[e2]Franck Cassez, Ralf Huuck, Gerwin Klein, Bastian Schlich (Eds.): Proceedings Seventh Conference on Systems Software Verification. EPTCS 102, 2012- 2011
[c24]Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein: seL4 Enforces Integrity. ITP 2011: 325-340- 2010
[j13]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): 107-115 (2010)
[c23]
[c22]
[c21]Ihor Kuz, Gerwin Klein, Corey Lewis, Adam Walker: capDL: a language for describing capability-based systems. ApSys 2010: 31-36
[c20]
2000 – 2009
- 2009
[j12]Ralf Huuck, Gerwin Klein, Bastian Schlich: Preface. Electr. Notes Theor. Comput. Sci. 254: 1-3 (2009)
[j11]Gerwin Klein, Ralf Huuck, Bastian Schlich: Operating System Verification. J. Autom. Reasoning 42(2-4): 123-124 (2009)
[c19]Gerwin Klein, Philip Derrin, Kevin Elphinstone: Experience report: seL4: formally verifying a high-performance microkernel. ICFP 2009: 91-96
[c18]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: 207-220
[c17]
[c16]Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish: Mind the Gap. TPHOLs 2009: 500-515- 2008
[j10]Ralf Huuck, Gerwin Klein, Bastian Schlich: Preface. Electr. Notes Theor. Comput. Sci. 217: 1-3 (2008)
[c15]
[c14]David Cock, Gerwin Klein, Thomas Sewell: Secure Microkernels, State Monads and Scalable Refinement. TPHOLs 2008: 167-182
[c13]
[c12]Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone: Verified Protection Model of the seL4 Microkernel. VSTTE 2008: 99-114
[e1]Bernhard Beckert, Gerwin Klein (Eds.): 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- 2007
[j9]Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein, Stefan M. Petters: Towards trustworthy computing systems: taking microkernels to the next level. Operating Systems Review 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]- 2006
[j8]Gerwin Klein, Tobias Nipkow: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4): 619-695 (2006)
[c8]
[c7]Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, Manuel M. T. Chakravarty: Running the manual: an approach to high-assurance microkernel development. Haskell 2006: 60-71
[c6]Simon Winwood, Gerwin Klein, Manuel M. T. Chakravarty: On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors. LOPSTR 2006: 111-126- 2005
[j7]
[j6]Gerwin Klein: Verified Java Bytecode Verification (Verified Java Bytecode Verification). it - Information Technology 47(2): 107-110 (2005)
[c5]
[c4]- 2004
[j5]
[j4]Gerwin Klein, Martin Strecker: Verified bytecode verification and type-certifying compilation. J. Log. Algebr. Program. 58(1-2): 27-60 (2004)
[c3]Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz: Prototyping Proof Carrying Code. IFIP TCS 2004: 333-348- 2003
[j3]Gerwin Klein, Martin Wildmoser: Verified Bytecode Subroutines. J. Autom. Reasoning 30(3-4): 363-398 (2003)
[j2]Gerwin Klein, Tobias Nipkow: Verified bytecode verifiers. Theor. Comput. Sci. 3(298): 583-626 (2003)
[c2]- 2001
[j1]Gerwin Klein, Tobias Nipkow: Verified lightweight bytecode verification. Concurrency and Computation: Practice and Experience 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
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-10-02 11:16 CEST by the dblp team



