Thomas Sewell

ORCID

Publication Activity (10 Years)

Years Active: 2008-2024
Publications (10 Years): 15

Top Venues

ITP

Arch. Formal Proofs

Proc. ACM Program. Lang.

Bioinform.

University of New South Wales, Sydney, Australia (PHD)

Education History

University of New South Wales, Sydney, Australia

PHD

Publications

Matthew Brecknell, David Greenaway, Johannes Hölzl, Fabian Immler, Gerwin Klein, Rafal Kolanski, Japheth Lim, Michael Norrish, Norbert Schirmer, Salomon Sickert, Thomas Sewell, Harvey Tuch, Simon Wimmer
AutoCorres2. Arch. Formal Proofs 2024 (2024)
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami
CN: Verifying Systems C Code with Separation-Logic Refinement Types. Proc. ACM Program. Lang. 7 (POPL) (2023)
Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens
Cakes That Bake Cakes: Dynamic Computation in CakeML. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. ESOP (2022)
Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell
Candle: A Verified Implementation of HOL Light. ITP (2022)
Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, Gabriele Keller
Cogent: uniqueness types and certifying compilation. J. Funct. Program. 31 (2021)
Tobias Nipkow, Thomas Sewell
Proof pearl: Braun trees. CPP (2020)
Anthony Nash, Thomas Sewell, Rhys A. Farrer, Alireza Abdolrasouli, Jennifer M. G. Shelton, Matthew C. Fisher, Johanna Rhodes
MARDy: Mycology Antifungal Resistance Database. Bioinform. 34 (18) (2018)
Thomas Sewell, Felix Kam, Gernot Heiser
High-assurance timing analysis for a high-assurance real-time operating system. Real Time Syst. 53 (5) (2017)
Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein
A Framework for the Automatic Formal Verification of Refinement from Cogent to C. ITP (2016)
Thomas Sewell, Felix Kam, Gernot Heiser
Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis. RTAS (2016)
Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby C. Murray, Gerwin Klein, Gernot Heiser
CoGENT: Verifying High-Assurance File System Implementations. ASPLOS (2016)
Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, Gerwin Klein
COGENT: Certified Compilation for a Functional Systems Language. CoRR (2016)
Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby C. Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein
Refinement through restraint: bringing down the cost of verification. ICFP (2016)
Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk, Thomas Sewell
Finite Machine Word Library. Arch. Formal Proofs 2016 (2016)
Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser
Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32 (1) (2014)
Thomas Sewell
Formal Replay of Translation Validation for Highly Optimised C. VPT@CAV (2014)
Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis, Thomas Sewell
Formally Verified System Initialisation. ICFEM (2013)
Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. CPP (2011)
Gerwin Klein, Toby C. Murray, Peter Gammie, Thomas Sewell, Simon Winwood
Provable Security: How Feasible Is It? HotOS (2011)
Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein
seL4 Enforces Integrity. ITP (2011)
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
seL4: formal verification of an operating-system kernel. Commun. ACM 53 (6) (2010)
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish
Mind the Gap. TPHOLs (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, Simon Winwood
seL4: formal verification of an OS kernel. SOSP (2009)
David Cock, Gerwin Klein, Thomas Sewell
Secure Microkernels, State Monads and Scalable Refinement. TPHOLs (2008)

Thomas Sewell.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Thomas Sewell