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 seL4 verified microkernel and the CakeML verified compiler. 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, http://dx.doi.org/10.1145/2560537
    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, http://dx.doi.org/10.1145/2462156.2462183
  • 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, http://dx.doi.org/10.1145/2951913.2951940
    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, http://dx.doi.org/10.1007/978-3-319-43144-4_20
    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, http://dx.doi.org/10.1007/978-3-642-03359-9_34