Thomas Sewell - Senior Research Engineer
Trustworthy Embedded Systems Project
Research Interests
Thomas is interested in program verification, programming languages and operating systems. Specific interests include language semantics, refinement calculi, interactive theorem provers and proof automation approaches.
NICTA Projects
Thomas is working on the l4.verified project, which aims to prove the functional correctness of a high performance microkernel.
Qualifications
Thomas has a combined Bachelor of Engineering (Software Engineering) and Bachelor of Science (Pure Mathematics) degree from UNSW.
Contact Details
| Phone: | +61 2 83060602 |
|---|
| Email: | thomas.sewell@nicta.com.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! |
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! |
|
|
|
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish
Mind the gap: A verification framework for low-level C
Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August, 2009 |
2008
|
|
|
David Cock, Gerwin Klein and Thomas Sewell
Secure microkernels, state monads and scalable refinement
Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, Montreal, Canada, August, 2008 |
