Research
Software Systems

Publications

Best publications in the L4.verified project:

 

Publications of the L4.verified and L4pilot projects:

2014

Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014

2013

Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415-429, San Francisco, CA, May, 2013

2011

Abstract PDF Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325-340, Nijmegen, The Netherlands, August, 2011
Abstract PDF Rafal Kolanski
Verification of programs in virtual memory using separation logic
PhD Thesis, UNSW, Sydney, Australia, July, 2011

2010

Abstract PDF Gerwin Klein
From a verified kernel towards verified systems
Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS), pp. 21–33, Shanghai, China, November, 2010
Invited extended abstract.
Abstract PDF Gerwin Klein
The L4.verified project - next steps
Proceedings of Verified Software: Theories, Tools and Experiments 2010, pp. 86–96, Edinburgh, UK, August, 2010
Invited extended abstract.
Abstract PDF Gerwin Klein
A formally verified OS kernel. Now what?
Proceedings of the 1st International Conference on Interactive Theorem Proving, pp. 1–7, Edinburgh, UK, July, 2010
Invited extended abstract.
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an operating-system kernel
Communications of the ACM, Volume 53, Number 6, pp. 107-115, June, 2010
Research Highlights paper

2009

Abstract
Slides
PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207-220, Big Sky, MT, USA, October, 2009
Abstract PDF
Presentation Video
Gerwin Klein, Philip Derrin and Kevin Elphinstone
Experience report: seL4 — formally verifying a high-performance microkernel
Proceedings of the 14th International Conference on Functional Programming, pp. 91–96, Edinburgh, UK, August, 2009
Abstract PDF Rafal Kolanski and Gerwin Klein
Types, maps and separation logic
International Conference on Theorem Proving in Higher Order Logics, pp. 276-292, Munich, Germany, August, 2009
Abstract PDF Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish
Mind the gap: A verification framework for low-level C
International Conference on Theorem Proving in Higher Order Logics, pp. 500-515, Munich, Germany, August, 2009
Abstract PDF Gernot Heiser
Trusted ⇐ trustworthy ⇐ proof – position paper
Proceedings of the 2nd Conference on Future of Trust in Computing, pp. 55–59, Berlin, Germany, July, 2009
Abstract PDF Gerwin Klein
Operating system verification — an overview
Sādhanā, Volume 34, Number 1, pp. 27–69, February, 2009
Invited paper. Journal homepage.

2008

Abstract PDF Rafal Kolanski and Gerwin Klein
Mapped separation logic
Verified Software: Theories, Tools and Experiments, pp. 15-29, Toronto, Canada, October, 2008
Abstract PDF Harvey Tuch
Formal memory models for verifying C systems code
PhD Thesis, UNSW, Sydney, Australia, August, 2008
Abstract PDF Rafal Kolanski
A logic for virtual memory
Systems Software Verification, pp. 61-77, Sydney, Australia, July, 2008

2007

Abstract PDF Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan Petters
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, Volume 41, Number 4, pp. 3-11, December, 2007
Abstract PDF Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser
Towards a practical, verified kernel
Workshop on Hot Topics in Operating Systems, pp. 6, San Diego, CA, USA, May, 2007
Abstract PDF Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser
Verifying a high-performance micro-kernel
7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007
Abstract PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97-108, Nice, France, January, 2007

2006

Abstract PDF Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M. T. Chakravarty
Running the manual: An approach to high-assurance microkernel development
Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA, September, 2006
Abstract PDF Kevin Elphinstone, Gerwin Klein and Rafal Kolanski
Formalising a high-performance microkernel
Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), pp. 1-7, Seattle, USA, August, 2006
Abstract PDF Gerwin Klein and Rafal Kolanski
Formalising the L4 microkernel API
Computing: The Australasian Theory Symposium (CATS), pp. 53–68, Hobart, Australia, January, 2006

2005

Abstract PDF Harvey Tuch and Gerwin Klein
A unified memory model for pointers
Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 474–488, Montego Bay, Jamaica, December, 2005
Abstract PDF Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco
L4cars
3rd Embedded Security in Cars Conference (escar), Cologne, Germany, November, 2005
Abstract PDF Harvey Tuch, Gerwin Klein and Gernot Heiser
OS verification — now!
Proceedings of the 10th Workshop on Hot Topics in Operating Systems, pp. 7–12, Santa Fe, NM, USA, June, 2005
Abstract PDF Rafal Kolanski
A formal model of the L4 micro-kernel API using the B method
Technical Report Technical Report 05-00029-1, NICTA, 2005

2004

Abstract PDF Kevin Elphinstone
Future directions in the evolution of the L4 microkernel
Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004
Abstract PDF Harvey Tuch and Gerwin Klein
Verifying the L4 virtual memory subsystem
Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, pp. 73–97, Sydney, Australia, October, 2004
Abstract PDF Gerwin Klein and Harvey Tuch
Towards verified virtual memory in L4
TPHOLs Emerging Trends '04, pp. 16 pages, Park City, Utah, USA, September, 2004