Dr Thomas Sewell
Dr Thomas Sewell is a software verification expert working at CSE.
Dr Sewell has worked in the field of software verification since 2006, and has contributed to major verification projects, include the  and the . These were significant milestone projects in the field, and remain to this day some of the most substantial pieces of software to have been proven correct.
He worked for the Â鶹Éçmadou lab of the NICTA research organisation from 2006-2012, working mostly on seL4. He completed his PhD at Â鶹Éçmadou from 2013 - 2017, working on the binary analysis of seL4. He was a postdoc at Chalmers University in Sweden 2018-2020, working on dynamic evaluation in the CakeML environment. He then moved to Cambridge University in the UK and worked on CPU security proofs and proof systems for the C language in 2020-2024.
Dr Sewell returned to Â鶹Éçmadou in 2024, and rejoined the  where he is working on the Pancake language (part of the CakeML family) and proofs about systems running on seL4.
He is an expert user of the Isabelle/HOL theorem prover, and also the HOL4 system and SMT-based approaches. At Â鶹Éçmadou he teaches on topics such as theorem proving and programming language semantics.