Publications
Best publications in the L4.verified project:
|
 |
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) |
|
|
 |
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:
2012
|
|
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 |
|
|
|
Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski Challenges and experiences in managing large-scale proofs Conferences on Intelligent Computer Mathematics (CICM) / Mathematical Knowledge Management, None, 2012 The final publication is available at www.springerlink.com |
2011
|
|
|
Rafal Kolanski Verification of programs in virtual memory using separation logic, PhD Thesis, School of Computer Science and Engineering, University of NSW, Sydney 2052, Australia, 2011 |
2010
|
|
|
Gerwin Klein From a verified kernel towards verified systems Proceedings of the 8th Asian Symposium on Programming Languages and Systems, Shanghai, China, November, 2010 Invited extended abstract. |
|
|
|
June Andronick, David Greenaway and Kevin Elphinstone Towards proving security in the presence of large untrusted components Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada, October, 2010 |
|
|
|
David Cock Lyrebird – assigning meanings to machines Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada, October, 2010 |
|
|
|
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, Chicago, IL, USA, October, 2010 Invited paper |
|
|
|
Gerwin Klein The L4.verified project - next steps Proceedings of Verified Software: Theories, Tools and Experiments 2010, Edinburgh, UK, August, 2010 Invited extended abstract. |
|
|
|
Gerwin Klein A formally verified OS kernel. Now what? 1st International Conference on Interactive Theorem Proving, Edinburgh, UK, July, 2010 Invited extended abstract. |
|
|
Michael von Tessin Towards high-assurance multiprocessor virtualisation Proceedings of the 6th International Verification Workshop, Edinburgh, UK, July, 2010 |
|
|
|
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 |
|
|
|
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) |
|
|
 |
Gerwin Klein, Thomas Sewell and Simon Winwood Refinement in the formal verification of sel4 Springer-Verlag, March, 2010 |
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, 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 Trusted ⇐ trustworthy ⇐ proof—position paper Proceedings of the 2nd 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 Verified Software: Theories, Tools and Experiments 2008, Toronto, Canada, October, 2008 |
|
|
|
Rafal Kolanski and Gerwin Klein Mapped separation logic Proceedings of Verified Software: Theories, Tools and Experiments 2008, Toronto, Canada, October, 2008 |
|
|
|
David Cock Bitfields and tagged unions in C: verification through automatic generation Proceedings of the 5th International Verification Workshop, 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, Sydney, Australia, February, 2008 |
|
|
|
Harvey Tuch Structured types and separation logic Proceedings of the 3rd Workshop on Systems Software Verification, 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 Proceedings of the 4th International Verification Workshop, 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 |