seL4: Formal verification of an OS kernel
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.
Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009
Mind the gap: A verification framework for low-level C
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish.
Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August, 2009