Supporting Persistent Object Systems in a Single Address Space. - Kevin Elphinstone; Stephen Russell 004; Gernot Heiser; Jochen Liedtke (POS, 1996)

Guarded Page Tables on Mips R4600 OR An Exercise in Architecture-Dependent Micro Optimization. - Jochen Liedtke; Kevin Elphinstone (ACM SIGOPS Oper. Syst. Rev., 1996)

Achieved IPC Performance. - Jochen Liedtke; Kevin Elphinstone; Sebastian Schönberg; Hermann Härtig; Gernot Heiser; Nayeem Islam; Trent Jaeger (Workshop on Hot Topics in Operating Systems, 1997)

The Mungi Single-Address-Space Operating System. - Gernot Heiser; Kevin Elphinstone; Jerry Vochteloo; Stephen Russell 004; Jochen Liedtke (Softw. Pract. Exp., 1998)

Flexible Access Control using IPC Redirection. - Trent Jaeger; Kevin Elphinstone; Jochen Liedtke; Vsevolod Panteleenko; Yoonho Park (Workshop on Hot Topics in Operating Systems, 1999)

How To Schedule Unlimited Memory Pinning of Untrusted Processes Or Provisional Ideas about Service-Neutrality. - Jochen Liedtke; Volkmar Uhlig; Kevin Elphinstone; Trent Jaeger; Yoonho Park (Workshop on Hot Topics in Operating Systems, 1999)

The SawMill multiserver approach. - Alain Gefflaut; Trent Jaeger; Yoonho Park; Jochen Liedtke; Kevin Elphinstone; Volkmar Uhlig; Jonathon Tidswell; Luke Deller; Lars Reuther (ACM SIGOPS European Workshop, 2000)

Synchronous IPC over transparent monitors. - Trent Jaeger; Jonathon Tidswell; Alain Gefflaut; Yoonho Park; Kevin Elphinstone; Jochen Liedtke (ACM SIGOPS European Workshop, 2000)

Preliminary thoughts on memory-bus scheduling. - Jochen Liedtke; Marcus Völp; Kevin Elphinstone (ACM SIGOPS European Workshop, 2000)

The SawMill Framework for Virtual Memory Diversity. - Mohit Aron; Jochen Liedtke; Kevin Elphinstone; Yoonho Park; Trent Jaeger; Luke Deller (ACSAC, 2001)

User-Level Management of Kernel Memory. - Andreas Haeberlen; Kevin Elphinstone (Asia-Pacific Computer Systems Architecture Conference, 2003)

Initial Evaluation of a User-Level Device Driver Framework. - Kevin Elphinstone; Stefan Götz 004 (Asia-Pacific Computer Systems Architecture Conference, 2004)

User-Level Device Drivers: Achieved Performance. - Ben Leslie; Peter Chubb; Nicholas Fitzroy-Dale; Stefan Götz 004; Charles Gray; Luke Macpherson; Daniel Potts; Yue-Ting Shen; Kevin Elphinstone; Gernot Heiser (J. Comput. Sci. Technol., 2005)

Running the manual: an approach to high-assurance microkernel development. - Philip Derrin; Kevin Elphinstone; Gerwin Klein; David A. Cock; Manuel M. T. Chakravarty (Haskell, 2006)

Towards a Practical, Verified Kernel. - Kevin Elphinstone; Gerwin Klein; Philip Derrin; Timothy Roscoe; Gernot Heiser (HotOS, 2007)

Hype and Virtue. - Timothy Roscoe; Kevin Elphinstone; Gernot Heiser (HotOS, 2007)

Towards trustworthy computing systems: taking microkernels to the next level. - Gernot Heiser; Kevin Elphinstone; Ihor Kuz; Gerwin Klein; Stefan M. Petters (ACM SIGOPS Oper. Syst. Rev., 2007)

Kernel design for isolation and assurance of physical memory. - Dhammika Elkaduwe; Philip Derrin; Kevin Elphinstone (IIES@EuroSys, 2008)

Verified Protection Model of the seL4 Microkernel. - Dhammika Elkaduwe; Gerwin Klein; Kevin Elphinstone (VSTTE, 2008)

Experience report: seL4: formally verifying a high-performance microkernel. - Gerwin Klein; Philip Derrin; Kevin Elphinstone (ICFP, 2009)

Towards Real Multi-criticality Scheduling. - Stefan M. Petters; Martin Lawitzky; Ryan Heffernan; Kevin Elphinstone (RTCSA, 2009)

seL4: formal verification of an OS kernel. - Gerwin Klein; Kevin Elphinstone; Gernot Heiser; June Andronick; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (SOSP, 2009)

The road to trustworthy systems. - Gernot Heiser; June Andronick; Kevin Elphinstone; Gerwin Klein; Ihor Kuz; Leonid Ryzhyk (STC@CCS, 2010)

Towards Proving Security in the Presence of Large Untrusted Components. - June Andronick; David Greenaway; Kevin Elphinstone (SSV, 2010)

seL4: formal verification of an operating-system kernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Gernot Heiser; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (Commun. ACM, 2010)

Trustworthy Real-Time Systems. - Stefan M. Petters; Kevin Elphinstone; Gernot Heiser (Advances in Real-Time Systems, 2012)

Increasing the trustworthiness of commodity hardware through software. - Kevin Elphinstone; Yanyan Shen (DSN, 2013)

Application level ballooning for efficient server consolidation. - Tudor-Ioan Salomie; Gustavo Alonso; Timothy Roscoe; Kevin Elphinstone (EuroSys, 2013)

From L3 to seL4 what have we learnt in 20 years of L4 microkernels? - Kevin Elphinstone; Gernot Heiser (SOSP, 2013)

Comprehensive formal verification of an OS microkernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Toby C. Murray; Thomas Sewell; Rafal Kolanski; Gernot Heiser (ACM Trans. Comput. Syst., 2014)

For a Microkernel, a Big Lock Is Fine. - Sean Peters; Adrian Danis; Kevin Elphinstone; Gernot Heiser (APSys, 2015)

Microkernel Mechanisms for Improving the Trustworthiness of Commodity Hardware. - Yanyan Shen; Kevin Elphinstone (EDCC, 2015)

An Evaluation of Coarse-Grained Locking for Multicore Microkernels. - Kevin Elphinstone; Amirreza Zarrabi; Adrian Danis; Yanyan Shen; Gernot Heiser (CoRR, 2016)

L4 Microkernels: The Lessons from 20 Years of Research and Deployment. - Gernot Heiser; Kevin Elphinstone (ACM Trans. Comput. Syst., 2016)

A Performance Evaluation of Rump Kernels as a Multi-server OS Building Block on seL4. - Kevin Elphinstone; Amirreza Zarrabi; Kent McLeod; Gernot Heiser (APSys, 2017)

Fault Tolerance Through Redundant Execution on COTS Multicores: Exploring Trade-Offs. - Yanyan Shen; Gernot Heiser; Kevin Elphinstone (DSN, 2019)