Implementation of Fast Address-Space Switching and TLB Sharing on the StrongARM Processor. - Adam Wiggins; Harvey Tuch; Volkmar Uhlig; Gernot Heiser (Asia-Pacific Computer Systems Architecture Conference, 2003)

Legba: Fast Hardware Support for Fine-Grained Protection. - Adam Wiggins; Simon Winwood; Harvey Tuch; Gernot Heiser (Asia-Pacific Computer Systems Architecture Conference, 2003)

OS Verification - Now! - Harvey Tuch; Gerwin Klein; Gernot Heiser (HotOS, 2005)

A Unified Memory Model for Pointers. - Harvey Tuch; Gerwin Klein (LPAR, 2005)

Types, bytes, and separation logic. - Harvey Tuch; Gerwin Klein; Michael Norrish (POPL, 2007)

Structured Types and Separation Logic. - Harvey Tuch (SSV, 2008)

Formal memory models for verifying C systems code. - Harvey Tuch (2008)

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)

Formal Verification of C Systems Code. - Harvey Tuch (J. Autom. Reason., 2009)

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)

The VMware mobile virtualization platform: is that a hypervisor in your pocket? - Kenneth C. Barr; Prashanth P. Bungale; Stephen Deasy; Viktor Gyuris; Perry Hung; Craig Newell; Harvey Tuch; Bruno Zoppis (ACM SIGOPS Oper. Syst. Rev., 2010)

Block storage virtualization with commodity secure digital cards. - Harvey Tuch; Cyprien Laplace; Kenneth C. Barr; Bi Wu (VEE, 2012)

AutoCorres2. - Matthew Brecknell; David Greenaway; Johannes Hölzl; Fabian Immler; Gerwin Klein; Rafal Kolanski; Japheth Lim; Michael Norrish; Norbert Schirmer; Salomon Sickert; Thomas Sewell; Harvey Tuch; et al. (Arch. Formal Proofs, 2024)