Publications

Best publications in the L4.verified project:

		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!
		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:

2009

		Gerwin Klein Correct OS kernel? Proof? Done! USENIX ;login:, 34(6), 28–34, (December, 2009)
		Andrew Boyton A verified shared capability model Proceedings of the 4th Workshop on Systems Software Verification SSV'09, Aachen, Germany, October, 2009
		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!
		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
		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
		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
		Gernot Heiser Trustworthy ⇐ trusted ⇐ proof—position paper Proceedings of the 1st Conference on Future of Trust in Computing, Berlin, Germany, July, 2009
		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)
		Gerwin Klein Operating system verification — an overview Sādhanā, 34(1), 27–69, (February, 2009) Invited paper. Journal homepage.

2008

		Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Proceedings of VSTTE 2008 — Verified Software: Theories, Tools and Experiments, Toronto, Canada, October, 2008
		Rafal Kolanski and Gerwin Klein Mapped separation logic Proceedings of VSTTE 2008 — Verified Software: Theories, Tools and Experiments, Toronto, Canada, October, 2008
		David Cock Bitfields and tagged unions in C: verification through automatic generation Proceedings of the 5th International Verification Workshop (VERIFY'08), Sydney, Australia, August, 2008
		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
		Harvey Tuch Formal memory models for verifying C systems code, PhD Thesis, School of Computer Science and Engineering, University of NSW, Sydney 2052, Australia, 2008
		Rafal Kolanski A logic for virtual memory Proceedings of the 3rd Workshop on Systems Software Verification SSV'08, Sydney, Australia, February, 2008
		Harvey Tuch Structured types and separation logic Proceedings of the 3rd Workshop on Systems Software Verification SSV'08, Sydney, Australia, February, 2008

2007

		Gernot Heiser Your system is secure? Prove it! USENIX ;login:, 32(6), 35–38, (December, 2007)
		Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Technical Report NRL-1474, NICTA, October, 2007
		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)
		Jia Meng, Lawrence C. Paulson and Gerwin Klein A termination checker for Isabelle Hoare logic 4th International Verification Workshop - VERIFY'07, Bremen, Germany, July, 2007
		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
		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
		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

		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
		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
		Rafal Kolanski and Gerwin Klein Formalising the L4 microkernel API Computing: The Australasian Theory Symposium (CATS 06), Hobart, Australia, January, 2006

2005

		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
		Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco L4cars 3rd Embedded Security in Cars Conference (escar), Cologne, Germany, November, 2005
		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
		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

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