Seminal seL4 Publications
A selection of key research articles about the seL4 technology, its design principles, verification, and applications.
Time protection: The missing OS abstraction
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser
EuroSys Conference, Dresden, Germany, pp. 1:1-1:17, March, 2019
Best Paper Award
Formally verified software in the real world
Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez
Communications of the ACM (CACM), Volume 61, Issue 10, pp. 68-77, October, 2018
Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time
Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser
EuroSys Conference, Porto, Portugal, pp. 26:1-26:16, April, 2018
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
Thomas Sewell, Chi Kam and Gernot Heiser
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, pp. 185-195, April, 2016
Outstanding Paper Award
Comprehensive formal verification of an OS microkernel
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
ACM Transactions on Computer Systems (TOCs), Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Translation validation for a verified OS kernel
Thomas Sewell, Magnus Myreen and Gerwin Klein
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 471-481, Seattle, Washington, USA, June, 2013
seL4: From general purpose to a proof of information flow enforcement
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
IEEE Symposium on Security and Privacy (S & P), pp. 415-429, San Francisco, CA, USA, May, 2013
Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
International Conference on Interactive Theorem Proving (ITP), pp. 325-340, Nijmegen, The Netherlands, August, 2011
seL4: Formal verification of an operating-system kernel
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
Communications of the ACM (CACM), Volume 53, Number 6, pp. 107-115, June, 2010
Research Highlights paper
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
ACM Symposium on Operating Systems Principles (SOSP), pp. 207-220, Big Sky, MT, USA, October, 2009
Best Paper Award, Hall of Fame Award