Harvey Tuch

Harvey Tuch, Cyprien Laplace, Kenneth C. Barr, Bi Wu: Block storage virtualization with commodity secure digital cards. VEE 2012: 191-202

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

Kenneth C. Barr, Prashanth P. Bungale, Stephen Deasy, Viktor Gyuris, Perry Hung, Craig Newell, Harvey Tuch, Bruno Zoppis: The VMware mobile virtualization platform: is that a hypervisor in your pocket? Operating Systems Review 44(4): 124-135 (2010)

Harvey Tuch: Formal Verification of C Systems Code. J. Autom. Reasoning 42(2-4): 125-187 (2009)

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood: seL4: formal verification of an OS kernel. SOSP 2009: 207-220

Harvey Tuch: Structured Types and Separation Logic. Electr. Notes Theor. Comput. Sci. 217: 41-59 (2008)

Harvey Tuch, Gerwin Klein, Michael Norrish: Types, bytes, and separation logic. POPL 2007: 97-108

Harvey Tuch, Gerwin Klein, Gernot Heiser: OS Verification - Now! HotOS 2005

Harvey Tuch, Gerwin Klein: A Unified Memory Model for Pointers. LPAR 2005: 474-488

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

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