Thomas Sewell
Thomas Sewell
Senior Research Associate, Cambridge University
Bestätigte E-Mail-Adresse bei - Startseite
Zitiert von
Zitiert von
seL4: Formal verification of an OS kernel
G Klein, K Elphinstone, G Heiser, J Andronick, D Cock, P Derrin, ...
Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles …, 2009
Comprehensive formal verification of an OS microkernel
G Klein, J Andronick, K Elphinstone, T Murray, T Sewell, R Kolanski, ...
ACM Transactions on Computer Systems (TOCS) 32 (1), 1-70, 2014
Translation validation for a verified OS kernel
TAL Sewell, MO Myreen, G Klein
Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013
Cogent: Verifying high-assurance file system implementations
S Amani, A Hixon, Z Chen, C Rizkallah, P Chubb, L O'Connor, J Beeren, ...
ACM SIGARCH Computer Architecture News 44 (2), 175-188, 2016
seL4 enforces integrity
T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein
International Conference on Interactive Theorem Proving, 325-340, 2011
Secure microkernels, state monads and scalable refinement
D Cock, G Klein, T Sewell
Theorem Proving in Higher Order Logics: 21st International Conference …, 2008
Mind the gap: A verification framework for low-level C
S Winwood, G Klein, T Sewell, J Andronick, D Cock, M Norrish
Theorem Proving in Higher Order Logics: 22nd International Conference …, 2009
Refinement through restraint: Bringing down the cost of verification
L O'Connor, Z Chen, C Rizkallah, S Amani, J Lim, T Murray, Y Nagashima, ...
ACM SIGPLAN Notices 51 (9), 89-102, 2016
Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL
S Böhme, ACJ Fox, T Sewell, T Weber
Certified Programs and Proofs: First International Conference, CPP 2011 …, 2011
A Framework for the Automatic Formal Verification of Refinement from Cogent to C
C Rizkallah, J Lim, Y Nagashima, T Sewell, Z Chen, L O’Connor, T Murray, ...
International Conference on Interactive Theorem Proving, 323-340, 2016
Verified security for the Morello capability-enhanced prototype Arm architecture
T Bauereiss, B Campbell, T Sewell, A Armstrong, L Esswood, I Stark, ...
European Symposium on Programming, 174-203, 2022
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
T Sewell, F Kam, G Heiser
2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS …, 2016
Refinement in the formal verification of the seL4 microkernel
G Klein, T Sewell, S Winwood
Design and Verification of Microprocessor Systems for High-Assurance …, 2010
High-assurance timing analysis for a high-assurance real-time operating system
T Sewell, F Kam, G Heiser
Real-Time Systems 53 (5), 812-853, 2017
Cogent: uniqueness types and certifying compilation
L O’CONNOR, Z Chen, C Rizkallah, V Jackson, S Amani, G Klein, ...
Journal of Functional Programming 31, e25, 2021
Formally verified system initialisation
A Boyton, J Andronick, C Bannister, M Fernandez, X Gao, D Greenaway, ...
Formal Methods and Software Engineering: 15th International Conference on …, 2013
COGENT: certified compilation for a functional systems language
L O'Connor, C Rizkallah, Z Chen, S Amani, J Lim, Y Nagashima, T Sewell, ...
arXiv preprint arXiv:1601.05520, 2016
Provable Security: How feasible is it?
G Klein, T Murray, P Gammie, T Sewell, S Winwood
13th Workshop on Hot Topics in Operating Systems (HotOS XIII), 2011
Candle: A verified implementation of HOL Light
O Abrahamsson, MO Myreen, R Kumar, T Sewell
13th International Conference on Interactive Theorem Proving (ITP 2022), 2022
CN: Verifying systems C code with separation-logic refinement types
C Pulte, DC Makwana, T Sewell, K Memarian, P Sewell, N Krishnaswami
Proceedings of the ACM on Programming Languages 7 (POPL), 1-32, 2023
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20