Thomas Sewell

According to our database, Thomas Sewell authored at least 27 papers between 2008 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

CN: Verifying Systems C Code with Separation-Logic Refinement Types.

Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami

Proc. ACM Program. Lang., January, 2023

Cakes That Bake Cakes: Dynamic Computation in CakeML.

Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens

Proc. ACM Program. Lang., 2023

2022

Candle: A Verified Implementation of HOL Light.

Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture.

Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell

Proceedings of the Programming Languages and Systems, 2022

2021

Cogent: uniqueness types and certifying compilation.

Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, Gabriele Keller

J. Funct. Program., 2021

2020

Proof pearl: Braun trees.

Tobias Nipkow, Thomas Sewell

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2018

MARDy: Mycology Antifungal Resistance Database.

Anthony Nash, Thomas Sewell, Rhys A. Farrer, Alireza Abdolrasouli, Jennifer M. G. Shelton, Matthew C. Fisher, Johanna Rhodes

Bioinform., 2018

2017

Translation validation for verified, efficient and timely operating systems.

Thomas Sewell

PhD thesis, 2017

High-assurance timing analysis for a high-assurance real-time operating system.

Thomas Sewell, Felix Kam, Gernot Heiser

Real Time Syst., 2017

2016

COGENT: Certified Compilation for a Functional Systems Language.

Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, Gerwin Klein

CoRR, 2016

Finite Machine Word Library.

Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk, Thomas Sewell

Arch. Formal Proofs, 2016

Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis.

Thomas Sewell, Felix Kam, Gernot Heiser

Proceedings of the 2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), 2016

A Framework for the Automatic Formal Verification of Refinement from Cogent to C.

Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein

Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

Refinement through restraint: bringing down the cost of verification.

Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby C. Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

CoGENT: Verifying High-Assurance File System Implementations.

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

Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, 2016

2014

Comprehensive formal verification of an OS microkernel.

Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser

ACM Trans. Comput. Syst., 2014

Formal Replay of Translation Validation for Highly Optimised C.

Thomas Sewell

Proceedings of the VPT 2014. Second International Workshop on Verification and Program Transformation, 2014

2013

Translation validation for a verified OS kernel.

Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Formally Verified System Initialisation.

Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis, Thomas Sewell

Proceedings of the Formal Methods and Software Engineering, 2013

2011

seL4 Enforces Integrity.

Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Provable Security: How Feasible Is It?

Gerwin Klein, Toby C. Murray, Peter Gammie, Thomas Sewell, Simon Winwood

Proceedings of the 13th Workshop on Hot Topics in Operating Systems, 2011

Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL.

Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

seL4: formal verification of an operating-system kernel.

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

Commun. ACM, 2010

Refinement in the Formal Verification of the seL4 Microkernel.

Gerwin Klein, Thomas Sewell, Simon Winwood

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009

Mind the Gap.

Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David A. Cock, Michael Norrish

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

seL4: formal verification of an OS kernel.

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

Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

2008

Secure Microkernels, State Monads and Scalable Refinement.

David A. Cock, Gerwin Klein, Thomas Sewell

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008