ÐÓ°ÉÂÛ̳
Back to
Dr Thomas Sewell

Dr Thomas Sewell

Lecturer
Engineering
Computer Science and Engineering

Thomas is a software verification expert working at CSE.

Thomas has worked in the field of software verification since 2006, and has contributed to major verification projects, include the and the . He completed his PhD at UNSW in 2017, working on the binary analysis of seL4. He worked at Chalmers University in Sweden 2018-2020 and at Cambridge University in the UK 2020-2024 before returning to UNSW.

Ìý
  • Journal articles | 2014
    Klein G; Andronick J; Elphinstone K; Murray T; Sewell T; Kolanski R; Heiser G, 2014, 'Comprehensive Formal Verification of an OS Microkernel', ACM Transactions on Computer Systems, 32,
    Journal articles | 2013
    Sewell T; Myreen M; Klein G, 2013, 'Translation validation for a verified OS kernel', Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 471 - 481,
  • Conference Papers | 2016
    O'Connor L; Chen Z; Rizkallah C; Amani S; Lim J; Murray T; Nagashima Y; Sewell T; Klein G, 2016, 'Refinement Through Restraint: Bringing down the cost of Verification', in Garrigue J; Keller G; Sumii E (eds.), International Conference on Functional Programming, ACM New York NY, USA, Nara, Japan, pp. 89 - 102, presented at International Conference on Functional Programming, Nara, Japan, 19 September 2016 - 21 September 2016,
    Conference Papers | 2016
    Rizkallah C; Lim J; Nagashima Y; Sewell T; Chen Z; O Connor L; Murray T; Keller G; Klein G; O'Connor-Davis L, 2016, 'A framework for the automatic formal verification of refinement from COGENT to C', in Blanchette JC; Merz S (ed.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, Nancy, France, pp. 323 - 340, presented at 7th International Conference, ITP 2016, Nancy, France, 22 August 2016 - 25 August 2016,
    Conference Papers | 2009
    Winwood SJ; Klein G; Sewell TA; Andronick J; Cock D; Norrish M, 2009, 'Mind the gap: A verification framework for low-level C', in Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Springer, Germany, presented at Theorem Proving in Higher Order Logics - TPHOL`s, Munich, Germany, 17 August 2009 - 20 August 2009,

  • 2022: ACM Software Systems award, together with the original seL4 team, for the seL4 verification project
  • 2019: ACM SIGOPS Hall of Fame award, together with the seL4 team, for the paper ''seL4: Formal Verification of an OS Kernel''
  • 2019: CORE John Makepeace Bennett Award for a Distinguished Doctoral Dissertation