By Dr Thomas Arthur Leck Sewell

Journal articles

Klein G; Andronick J; Elphinstone K; Murray T; Sewell T; Kolanski R; Heiser G, 2014, 'Comprehensive Formal Verification of an OS Microkernel', ACM Transactions on Computer Systems, 32, http://dx.doi.org/10.1145/2560537

Sewell T; Myreen M; Klein G, 2013, 'Translation validation for a verified OS kernel', Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI, pp. 471 - 481, http://dx.doi.org/10.1145/2462156.2462183

Conference Papers

O'Connor L; Chen Z; Rizkallah C; Amani S; Lim J; Murray T; Nagashima Y; Sewell T; Klein G, 2016, 'Refinement Through Restraint: Bringing down the cost of Verification', in Garrigue J; Keller G; Sumii E (eds.), International Conference on Functional Programming, ACM New York NY, USA, Nara, Japan, pp. 89 - 102, presented at International Conference on Functional Programming, Nara, Japan, 19 September 2016 - 21 September 2016, http://dx.doi.org/10.1145/2951913.2951940

Rizkallah C; Lim J; Nagashima Y; Sewell T; Chen Z; O Connor L; Murray T; Keller G; Klein G, 2016, 'A framework for the automatic formal verification of refinement from COGENT to C', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Nancy, France, pp. 323 - 340, presented at 7th International Conference, ITP 2016, Nancy, France, 22 August 2016 - 25 August 2016, http://dx.doi.org/10.1007/978-3-319-43144-4_20

Winwood SJ; Klein G; Sewell TA; Andronick J; Cock D; Norrish M, 2009, 'Mind the gap: A verification framework for low-level C', in Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Springer, Germany, presented at Theorem Proving in Higher Order Logics - TPHOL`s, Munich, Germany, 17 August 2009 - 20 August 2009, http://dx.doi.org/10.1007/978-3-642-03359-9_34

Back to profile page