Thomas Sewell

I am an expert in software verification and proof engineering. I have worked on a number of large verification projects, including:

• The verification of the seL4 microkernel.
• Correctness of the compiled binary of seL4, my PhD project.
• Adding dynamic evaluation to CakeML, a verified language in the ML family.
• Verifying the security properties of the Morello instance of the CHERI hardware security extension.

Publication lists can be found on Google Scholar.

At UNSW I am teaching software verification ( COMP 4161 ), programming languages ( COMP 3161/9164 ), and operating systems ( COMP 3231/3891/9201/9283 ).

I am continuing to work on proofs about the seL4 microkernel and the Pancake language ( more info here ). Much of this work is in conjunction with the Trustworthy Systems group.

Contact: firstname.lastname@unsw.edu.au