|
 |
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
Structured types and separation logic
3rd International Workshop on Systems Software Verification (SSV08), Sydney, Australia, February, 2008 |
|
|
|
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 , 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 |
|
|
|
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 |
|
|
|
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
Embedded Security in Cars (escar 2005) Workshop, 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 |
|
|
|
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 |
