Harvey Tuch

According to our database, Harvey Tuch authored at least 13 papers between 2003 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

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, Simon Wimmer

Arch. Formal Proofs, 2024

2012

Block storage virtualization with commodity secure digital cards.

Harvey Tuch, Cyprien Laplace, Kenneth C. Barr, Bi Wu

Proceedings of the 8th International Conference on Virtual Execution Environments, 2012

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

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, Simon Winwood

Commun. ACM, 2010

2009

Formal Verification of C Systems Code.

Harvey Tuch

J. Autom. Reason., 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, Simon Winwood

Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

2008

Formal memory models for verifying C systems code.

Harvey Tuch

PhD thesis, 2008

Structured Types and Separation Logic.

Harvey Tuch

Proceedings of the 3rd International Workshop on Systems Software Verification, 2008

2007

Types, bytes, and separation logic.

Harvey Tuch, Gerwin Klein, Michael Norrish

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

2005

A Unified Memory Model for Pointers.

Harvey Tuch, Gerwin Klein

Proceedings of the Logic for Programming, 2005

OS Verification - Now!

Harvey Tuch, Gerwin Klein, Gernot Heiser

Proceedings of HotOS'05: 10th Workshop on Hot Topics in Operating Systems, 2005

2003

Legba: Fast Hardware Support for Fine-Grained Protection.

Adam Wiggins, Simon Winwood, Harvey Tuch, Gernot Heiser

Proceedings of the Advances in Computer Systems Architecture, 2003

Implementation of Fast Address-Space Switching and TLB Sharing on the StrongARM Processor.

Adam Wiggins, Harvey Tuch, Volkmar Uhlig, Gernot Heiser

Proceedings of the Advances in Computer Systems Architecture, 2003