Thomas Sewell

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