Thomas Sewell

Research Engineer

NICTA/Chalmers University of Technology

Show Academic Trajectory

Ego Network

D-Core

Research Interests

Author Statistics

Experience

Education

Bio

Thomas was a key proof engineer and maintainer on the NICTA/Data61 seL4 verification project, and is now a postdoc at Chalmers University, working on CakeML.
Research interests:
Formal Methods, Interactive Proof Systems, Compilers

Papers23 papers

Sort

By YearBy Citation

Translation validation for verified, efficient and timely operating systems

Thomas Sewell

(2017)

EIBibtex

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

Thomas Sewell, Felix Kam,Gernot Heiser

Real-Time Systems, no. 5 (2017): 812-853

Cited by11EIBibtex

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

ICFP, pp.89-102, (2016)

Cited by31EIBibtex

Refinement through restraint: bringing down the cost of verification

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

Special Interest Group on Programming Languages, no. 9 (2016): 89-102

Cited by31EIBibtex

Finite Machine Word Library

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

Archive of Formal Proofs, (2016)

EIBibtex

Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis

Thomas Sewell, Felix Kam,Gernot Heiser

RTAS, (2016)

Cited by13EIBibtex

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

Special Interest Group on Programming Languages, no. 4 (2016): 175-188

Cited by69EIBibtex

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

Architectural Support for Programming Languages and Operating Systems, no. 2 (2016): 175-188

Cited by69EIBibtex

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

ITP, pp.323-340, (2016)

Cited by6EIBibtex

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

arXiv: Programming Languages, (2016)

Cited by8EIBibtex

Comprehensive formal verification of an OS microkernel

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

ACM Trans. Comput. Syst., no. 1 (2014)

Cited by232EIBibtex

Formally Verified System Initialisation

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

Lecture Notes in Computer Science, (2013): 70-85

Cited by17EIBibtex

Translation validation for a verified OS kernel

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

PLDI, no. 6 (2013): 471-482

Cited by84EIBibtex

Reconstruction of z3's bit-vector proofs in HOL4 and Isabelle/HOL

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

CPP, pp.183-198, (2011)

Cited by14EIBibtex

Provable Security: how feasible is it

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

HotOS, pp.28-28, (2011)

Cited by12EIBibtex

seL4 enforces integrity

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

ITP, pp.325-340, (2011)

Cited by79EIBibtex

Refinement in the Formal Verification of the seL4 Microkernel

Gerwin Klein,Thomas Sewell,Simon Winwood

(2010)

Cited by7Bibtex

seL4: formal verification of an operating-system kernel

Gerwin Klein,June Andronick,Kevin Elphinstone,Gernot Heiser,David Cock,Philip Derrin,Dhammika Elkaduwe,Kai Engelhardt,Rafal Kolanski,Michael Norrish,Thomas Sewell,Harvey Tuch

Commun. ACM, no. 6 (2010): 107-115

Cited by1526EIBibtex

seL4: formal verification of an OS kernel

Gerwin Klein,Kevin Elphinstone,Gernot Heiser,June Andronick,David Cock,Philip Derrin,Dhammika Elkaduwe,Kai Engelhardt,Rafal Kolanski,Michael Norrish,Thomas Sewell,Harvey Tuch

SOSP, pp.207-220, (2009)

Cited by1828EIBibtex

Mind the Gap A Verification Framework for Low-Level C

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

(2009)

Cited by25Bibtex

View All

Base Info Papers Patents Projects

Thomas SewellBinding

Papers23 papers

Thomas Sewell