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
|
 |
Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Haburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwartz and Yuval Yarom Spectre attacks: Exploiting speculative execution IEEE Symposium on Security and Privacy, pp. 19-37, San Francisco, May, 2019 Distinguished Paper Award! |
|
 |
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser Time protection: The missing OS abstraction EuroSys Conference, Dresden, Germany, March, 2019 Best Paper Award! |
|
|
|
Moritz Lipp, Michael Schwartz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom and Mike Hamburg Meltdown: reading kernel memory from user space USENIX Security Symposium, pp. -, Baltimore, MD, USA, August, 2018 |
|
|
|
Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time EuroSys Conference, Porto, Portugal, April, 2018 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Aaron Carroll and Gernot Heiser An analysis of power consumption in a smartphone USENIX Annual Technical Conference, pp. 271–284, Boston, MA, US, 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 ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009 Best Paper Award! Hall of Fame Award! |
|
|
|
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 |
|
|
|
Dave Snowdon, Etienne Le Sueur, Stefan Petters and Gernot Heiser Koala: A platform for OS-level power management EuroSys Conference, pp. 289–302, Nuremberg, DE, April, 2009 |