publications

(also available as [bibtex])

seL4: Formal Verification of an OS Kernel (conference)
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood. seL4: Formal Verification of an OS Kernel. Proc. SOSP'09, pages 207-220, ACM 2009. Best Paper Award.
[pdf] [bibtex]
Experience report: seL4 — Formally Verifying a High-Performance Microkernel (conference)
G. Klein, P. Derrin, K. Elphinstone. Experience report: seL4 — Formally Verifying a High-Performance Microkernel. In: A. Tolmach, Proc. ICFP'09, pages 91-96. ACM 2009.
[pdf] [bibtex]
Mind the Gap: A Verification Framework for Low-Level C (conference)
S. Winwood, G. Klein, T. Sewell, J. Andronick, D. Cock, M. Norrish. Mind the Gap: A Verification Framework for Low-Level C. In: S. Berghofer, T. Nipkow, C. Urban, M. Wenzel. Proc. TPHOLs'09, volume 5674 of Lecture Notes in Computer Science, pages 500-515, Springer 2009.
[pdf] [bibtex]
Types, Maps, and Separation Logic (conference)
R. Kolanski, G. Klein. Types, Maps, and Separation Logic. In: S. Berghofer, T. Nipkow, C. Urban, M. Wenzel. Proc. TPHOLs'09, volume 5674 of Lecture Notes in Computer Science, pages 276-292, Springer 2009.
[pdf] [bibtex]
Operating System Verification — An Overview (journal)
G. Klein. Operating System Verification — An Overview. Sādhanā 34(1), pages 26-69, 2009. Invited paper.
[pdf] [bibtex]
Mapped Separation Logic (conference)
R. Kolanski and G. Klein.. Mapped Separation Logic. In: J. Woodcock and N. Shankar, Proc. 2nd IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2008), volume 5295 of Lecture Notes in Computer Science, pages 15-29, Springer. 2008.
[pdf] [bibtex]
Verified Protection Model of the seL4 Microkernel (conference)
D. Elkaduwe, G. Klein., and K. Elphinstone. Verified Protection Model of the seL4 Microkernel. In: J. Woodcock and N. Shankar, Proc. 2nd IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2008), volume 5295 of Lecture Notes in Computer Science, pages 99-114, Springer. 2008.
[pdf] [bibtex]
Secure Microkernels, State Monads and Scalable Refinement (conference)
D. Cock, G. Klein, and T. Sewell. Secure Microkernels, State Monads and Scalable Refinement. In: O. Ait, C. Munoz, and S. Tahar (eds), Proc. TPHOLs'08, volume 5170 of Lecture Notes in Computer Science, pages 167-182, 2008.
[pdf] [bibtex]
Proc. 5th International Verification Workshop (VERIFY'08) (proceedings)
B. Beckert and G. Klein (eds). Proceedings of the 5th International Verification Workshop (VERIFY'08). Volume 372 of CEUR Workshop Proceedings, 2008.
[pdf] [bibtex]
Proc. 3rd International Workshop on Systems Software Verification (SSV'08) (proceedings)
R. Huuck, G. Klein, and B. Schlich (eds). Proceedings of the 3rd International Workshop on Systems Software Verification (SSV'08). Volume 217 of Electronic Notes in Computer Science, Elsevier 2008.
[Elsevier online version][bibtex]
A Termination Checker for Isabelle Hoare Logic (workshop)
J. Meng, L. C. Paulson, and G. Klein. A Termination Checker for Isabelle Hoare Logic. In: B. Beckert (ed), Proc. 4th International Verification Workshop - VERIFY'07, volume 259 of CEUR Workshop Proceeding, pages 104-118, Bremen, Germany, 2007.
[pdf] [bibtex]
Towards trustworthy computing systems: taking microkernels to the next level (journal)
G. Heiser, K. Elphinstone, I. Kuz, G. Klein, S. Petters. Towards trustworthy computing systems: taking microkernels to the next level. In: Operating Systems Review, 41(4), pages 3-11, 2007.
[pdf] [bibtex]
Towards a Practical, Verified Kernel (workshop)
K. Elphinstone, G. Klein, P. Derrin, T. Roscoe, and G. Heiser. Towards a Practical, Verified Kernel. In: Proc. 11th Workshop on Hot Topics in Operating Systems. 6 pages, 2007.
[pdf] [bibtex]
Types, Bytes, and Separation Logic (conference)
G. Klein, H. Tuch, and M. Norrish. Types, Bytes, and Separation Logic. In: M. Hofmann and M. Felleisen (eds), POPL'07. pages 97-108, 2007.
[pdf] [bibtex]
A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler (journal preprint)
G. Klein and T. Nipkow. A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler. In: TOPLAS. 28(4):619-695, 2006.
[pdf] [bibtex]
Formalising a High-Performance Microkernel (workshop)
K. Elphinstone, G. Klein, and R. Kolanski. Formalising a High-Performance Microkernel In: R. Leino (ed), Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Microsoft Research Technical Report MSR-TR-2006-117, pages 1-7, Aug 2006.
[pdf] [bibtex]
On the automated synthesis of proof-carrying temporal reference monitors (conference)
S. Winwood, G. Klein, and M. Chakravarty. On the automated synthesis of proof-carrying temporal reference monitors. In: Germán Puebla (ed), International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 06), volume 4407 of LNCS, pages 111-126, Springer, 2007.
[pdf] [bibtex]
Formalising the L4 microkernel API (conference)
R. Kolanski and G. Klein. Formalising the L4 microkernel API. In: B. Jay and J. Gudmundsson (ed), Computing: The Australasian Theory Symposium (CATS 06), volume 51 of Conferences in Research and Practice in Information Technology, pages 53-68, 2006.
[pdf] [bibtex]
A Unified Memory Model for Pointers (conference)
H. Tuch and G. Klein. A Unified Memory Model for Pointers. In: G. Sutcliffe and A. Voronkov (ed), 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-12), volume 3835 of Lecture Notes in Computer Science, pages 474-488, 2005.
[pdf] [bibtex]
OS Verification — now! (workshop)
H. Tuch, G. Klein and G. Heiser. OS Verification — now! In: Proc. 10th Workshop on Hot Topics in Operating Systems (HotOS X), 6 pages, 2005.
[pdf] [bibtex]
High Assurance System Software (workshop/position paper)
G. Klein and R. Huuck. High Assurance System Software. In: Tony Cant (ed), Proc. 10th Australian Workshop on Safety Critical Systems and Software (SCS'05), volume 55 of Conferences in Research and Practice in Information Technology, 9 pages, 2005.
[bibtex]
Proc. NICTA Formal Methods Workshop on OS Verification (workshop proceedings)
G. Klein (ed). Proc. NICTA Formal Methods Workshop on Operating Systems Verification, Technical Report 0401005T-1, National ICT Australia, 2004.
[pdf] [bibtex]
Verifying the L4 Virtual Memory Subsystem (workshop)
H. Tuch and G. Klein. Verifying the L4 Virtual Memory Subsystem. In: Proc. NICTA Formal Methods Workshop on Operating Systems Verification, Technical Report 0401005T-1, National ICT Australia, 2004.
[pdf] [bibtex]
Towards Verified Virtual Memory in L4 (emerging trends poster session)
G. Klein and H. Tuch. Towards Verified Virtual Memory in L4. In TPHOLs Emerging Trends '04, 2004.
[pdf] [bibtex]
Prototyping Proof Carrying Code (conference)
M. Wildmoser, T. Nipkow, G. Klein, and S. Nanz. Prototyping Proof Carrying Code. In Proc. 3rd IFIP Int. Conf. Theoretical Computer Science (TCS 2004), 2004.
[pdf] [bibtex]
A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler (technical report)
G. Klein and T. Nipkow. A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler. Technical Report 0400001T.1, National ICT Australia, Sydney, March 2004.
[pdf] [bibtex]
Verified Bytecode Verification and type-certifying Compilation (journal preprint)
G. Klein and M. Strecker. Verified Bytecode Verification and type-certifying Compilation. Journal of Logic Programming, 58(1-2):27-60, 2004.
[pdf] [bibtex]
Verified bytecode subroutines (conference)
G. Klein and M. Wildmoser. Verified bytecode subroutines. In David Basin and Burkhard Wolff, editors, Proceedings of Theorem Proving in Higher Order Logics, volume 2758 of Lecture Notes in Computer Science, pages 55-70, 2003.
[pdf] [bibtex]
Verified Java Bytecode Verification (PhD thesis)
G. Klein. Verified Java Bytecode Verification, PhD thesis, Institut für Informatik, Technische Universität München, 2003.
[pdf] [bibtex]
Verified Bytecode Subroutines (journal preprint)
G. Klein and M. Wildmoser. Verified Bytecode Subroutines. Journal of Automated Reasoning, 30(3-4):363-398, 2003.
[pdf] [bibtex]
Verified Bytecode Verifiers (journal preprint)
G. Klein and T. Nipkow. Verified bytecode verifiers. Theoretical Computer Science, 298(3):583-626, 2003.
[pdf] [bibtex]
Verified Lightweight Bytecode Verification (journal version, preprint)
G. Klein and T. Nipkow. Verified lightweight bytecode verification. Concurrency and Computation: Practice and Experience, 13(13):1133-1151, 2001.
[pdf] [bibtex]
Verified Lightweight Bytecode Verification (extended abstract)
G. Klein and T. Nipkow. Verified lightweight bytecode verification. In S. Drossopoulou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Proc. 2nd ECOOP Workshop on Formal Techniques for Java Programs. Technical Report 269, Fernuniversität Hagen, 2000.
[pdf] [bibtex]
FormGen: A generator for adaptive forms based on EasyGUI (conference)
A. Brandl and G. Klein. FormGen: A generator for adaptive forms based on EasyGUI. In H. Bullinger and J. Ziegler, editors, Human-Computer Interaction: Ergonomics and Userinterfaces. Proc. HCI'99, volume 1, pages 1172-1176. Lawrence Erlbaum Associates, 1999.
[pdf] [bibtex]
Generating graphical editors for graph-like datastructures (master's thesis)
G. Klein. Generating graphical editors for graph-like datastructures. Master's thesis, Chair of Computer Science II, Technische Universität München, 1999.
[pdf] [bibtex].