| 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 | 2785 | 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 | 492 | 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 | 203 | 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 | 128 | 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 | 119 | 2011 |
| Secure microkernels, state monads and scalable refinement D Cock, G Klein, T Sewell Theorem Proving in Higher Order Logics: 21st International Conference …, 2008 | 113 | 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 | 65 | 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 | 55 | 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 | 46 | 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 | 28 | 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 | 27 | 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 | 27 | 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 | 26 | 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 | 25 | 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 | 23 | 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 | 23 | 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 | 16 | 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 | 16 | 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 | 13 | 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 | 8 | 2023 |
