Publications

Best publications in the L4.verified project:

plain text 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, 53(6), 107–115, (June, 2010)
plain text 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
Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009
Best Paper Award!
plain text PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007

 

Publications of the L4.verified and L4pilot projects:

2012

plain text PDF Michael von Tessin
The clustered multikernel: An approach to formal verification of multiprocessor OS kernels
Proceedings of the 2nd Workshop on Systems for Future Multi-core Architectures, Bern, Switzerland, April, 2012

2011

plain text PDF Rafal Kolanski
Verification of programs in virtual memory using separation logic, PhD Thesis, School of Computer Science and Engineering, Sydney, Australia, 2011

2010

plain text PDF Gerwin Klein
From a verified kernel towards verified systems
Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS), Shanghai, China, November, 2010
Invited extended abstract.
plain text PDF June Andronick, David Greenaway and Kevin Elphinstone
Towards proving security in the presence of large untrusted components
Proceedings of the 5th Systems Software Verification, Vancouver, Canada, October, 2010
plain text PDF David Cock
Lyrebird – assigning meanings to machines
Proceedings of the 5th Systems Software Verification, Vancouver, Canada, October, 2010
plain text PDF Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk
The road to trustworthy systems
Proceedings of the 5th ACM Workshop on Scalable Trusted Computing (ACMSTC), Chicago, IL, USA, October, 2010
Invited paper
plain text PDF Gerwin Klein
The L4.verified project - next steps
Proceedings of Verified Software: Theories, Tools and Experiments 2010, Edinburgh, UK, August, 2010
Invited extended abstract.
plain text PDF Gerwin Klein
A formally verified OS kernel. Now what?
Proceedings of the 1st International Conference on Interactive Theorem Proving, Edinburgh, UK, July, 2010
Invited extended abstract.
plain text PDF Michael von Tessin
Towards high-assurance multiprocessor virtualisation
Proceedings of the 6th International Verification Workshop, Edinburgh, UK, July, 2010
plain text PDF June Andronick
From a proven correct microkernel to trustworthy large systems
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Paris, France, June, 2010
plain text 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, 53(6), 107–115, (June, 2010)
plain text to be published Gerwin Klein, Thomas Sewell and Simon Winwood
Refinement in the formal verification of seL4
Springer, March, 2010

2009

plain text PDF Gerwin Klein
Correct OS kernel? Proof? Done!
USENIX ;login:, 34(6), 28–34, (December, 2009)
plain text PDF Andrew Boyton
A verified shared capability model
Proceedings of the 4th Systems Software Verification, Aachen, Germany, October, 2009
plain text 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
Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009
Best Paper Award!
plain text 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, Edinburgh, UK, August, 2009
plain text PDF Rafal Kolanski and Gerwin Klein
Types, maps and separation logic
Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August, 2009
plain text PDF Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish
Mind the gap: A verification framework for low-level C
Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August, 2009
plain text PDF Gernot Heiser
Trusted ⇐ trustworthy ⇐ proof—position paper
Proceedings of the 2nd Conference on Future of Trust in Computing, Berlin, Germany, July, 2009
plain text PDF Harvey Tuch
Formal verification of C systems code: Structured types, separation logic and theorem proving
Journal of Automated Reasoning: Special Issue on Operating System Verification, 42(2–4), 125–187, (April, 2009)
plain text PDF Gerwin Klein
Operating system verification — an overview
Sādhanā, 34(1), 27–69, (February, 2009)
Invited paper. Journal homepage.

2008

plain text PDF Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Proceedings of Verified Software: Theories, Tools and Experiments 2008, Toronto, Canada, October, 2008
plain text PDF Rafal Kolanski and Gerwin Klein
Mapped separation logic
Proceedings of Verified Software: Theories, Tools and Experiments 2008, Toronto, Canada, October, 2008
plain text PDF David Cock
Bitfields and tagged unions in C: verification through automatic generation
Proceedings of the 5th International Verification Workshop, Sydney, Australia, August, 2008
plain text PDF David Cock, Gerwin Klein and Thomas Sewell
Secure microkernels, state monads and scalable refinement
Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, Montreal, Canada, August, 2008
plain text PDF Harvey Tuch
Formal memory models for verifying C systems code, PhD Thesis, School of Computer Science and Engineering, Sydney, Australia, 2008
plain text PDF Rafal Kolanski
A logic for virtual memory
Proceedings of the 3rd Systems Software Verification, Sydney, Australia, February, 2008
plain text PDF Harvey Tuch
Structured types and separation logic
Proceedings of the 3rd Systems Software Verification, Sydney, Australia, February, 2008

2007

plain text PDF Gernot Heiser
Your system is secure? Prove it!
USENIX ;login:, 32(6), 35–38, (December, 2007)
plain text PDF Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Technical Report NRL-1474, NICTA, October, 2007
plain text PDF Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, 41(4), 3–11, (July, 2007)
plain text PDF Jia Meng, Lawrence C. Paulson and Gerwin Klein
A termination checker for Isabelle Hoare logic
Proceedings of the 4th International Verification Workshop, Bremen, Germany, July, 2007
plain text PDF Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser
Towards a practical, verified kernel
Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007
plain text 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
plain text PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007

2006

plain text 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
plain text PDF Kevin Elphinstone, Gerwin Klein and Rafal Kolanski
Formalising a high-performance microkernel
Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Seattle, USA, August, 2006
plain text PDF Rafal Kolanski and Gerwin Klein
Formalising the L4 microkernel API
Computing: The Australasian Theory Symposium (CATS 06), Hobart, Australia, January, 2006

2005

plain text 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, Montego Bay, Jamaica, December, 2005
plain text 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
plain text PDF Harvey Tuch, Gerwin Klein and Gernot Heiser
OS verification — now!
Proceedings of the 10th Workshop on Hot Topics in Operating Systems, Santa Fe, NM, USA, June, 2005
plain text PDF Rafal Kolanski
A formal model of the L4 micro-kernel API using the B method
Technical Report Technical Report 05-00029-1, National ICT Australia, 2005

2004

plain text 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
plain text 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, Sydney, Australia, October, 2004
plain text PDF Gerwin Klein and Harvey Tuch
Towards verified virtual memory in L4
TPHOLs Emerging Trends '04, Park City, Utah, USA, September, 2004