Skip to main content

Our research areas

Trustworthy Systems features a unique combination of experts in operating systems, formal methods and programming language design. By working closely together, we have produced systems that are efficient and practical, while at the same time they are backed by rigorous theoretical guarantees.

Our best papers

See all publications

Abstract PDF Gernot Heiser and Kevin Elphinstone
L4 microkernels: The lessons from 20 years of research and deployment
ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016
Abstract PDF Thomas Sewell, Chi Kam and Gernot Heiser
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016
Outstanding Paper award
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Abstract
Slides
PDF Thomas Sewell, Magnus Myreen and Gerwin Klein
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013
Abstract
Slides
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013
Abstract
Slides
PDF Aaron Carroll and Gernot Heiser
An analysis of power consumption in a smartphone
USENIX Annual Technical Conference, pp. 271–284, Boston, MA, USA, June, 2010
Abstract
Slides
PDF
Presentation Video
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
ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009
Abstract PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser
Automatic device driver synthesis with Termite
ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009
Abstract PDF Dave Snowdon, Etienne Le Sueur, Stefan Petters and Gernot Heiser
Koala: A platform for OS-level power management
EuroSys Conference, pp. 289–302, Nuremburg, DE, April, 2009
Served by Apache on Linux on seL4.