Harvey Tuch - PhD Student
Trustworthy Embedded Systems Project
Research Interests
As a PhD student, Harvey worked on the application of formal verification techniques such as interactive theorem proving to systems software, in particular the L4 microkernel in the context of the L4.verified project. Other research interests include computer architecture, embedded systems and security.
NICTA Projects
L4.verified
Career Summary
Mr Tuch was an intern in the virtualisation research group at Intel, Oregon for 6 months at the end of 2005.
Qualifications
Mr Tuch was awarded a Bachelor of Engineering in Computer Engineering, with first class Honours, at the University of New South Wales in 2002. He is currently engaged in a PhD with the ERTOS group at NICTA.
Contact Details
| Email: | htuch@cse.unsw.edu.au |
|---|
More contact information is available at the
ERTOS Contacts page.
Publications
Best Papers
|
 |
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, 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
Communications of the ACM, 53(6), 107–115, (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
Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009
Best Paper Award! |
|
|
|
Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007 |
NICTA Papers
2010
|
|
|
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, 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
Communications of the ACM, 53(6), 107–115, (June, 2010) |
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 and Simon Winwood
seL4: Formal verification of an OS kernel
Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009
Best Paper Award! |
|
|
|
Harvey Tuch
Formal verification of C systems code: Structured types, separation logic and theorem proving
Journal of Automated Reasoning: Special Issue on Operating System Verification, 42(2–4), 125–187, (April, 2009) |
2008
|
|
|
Harvey Tuch
Formal memory models for verifying C systems code, PhD Thesis, School of Computer Science and Engineering, University of NSW, Sydney 2052, Australia, 2008
|
|
|
|
Harvey Tuch
Structured types and separation logic
Proceedings of the 3rd Workshop on Systems Software Verification, Sydney, Australia, February, 2008 |
2007
|
|
|
Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007 |
2005
|
|
|
Harvey Tuch and Gerwin Klein
A unified memory model for pointers
Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Montego Bay, Jamaica, December, 2005 |
|
|
|
Harvey Tuch, Gerwin Klein and Gernot Heiser
OS verification — now!
Proceedings of the 10th Workshop on Hot Topics in Operating Systems, Santa Fe, NM, USA, June, 2005 |
2004
|
|
|
Harvey Tuch and Gerwin Klein
Verifying the L4 virtual memory subsystem
Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004 |
|
|
|
Gerwin Klein and Harvey Tuch
Towards verified virtual memory in L4
TPHOLs Emerging Trends '04, Park City, Utah, USA, September, 2004 |
2003
|
|
 |
Adam Wiggins, Harvey Tuch, Volkmar Uhlig and Gernot Heiser
Implementation of fast address-space switching and TLB sharing on the StrongARM processor
Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003 |
|
|
|
Adam Wiggins, Simon Winwood, Harvey Tuch and Gernot Heiser
Legba: Fast hardware support for fine-grained protection
Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003 |
