| 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 | 2812 | 2009 |
| CakeML: a verified implementation of ML R Kumar, MO Myreen, M Norrish, S Owens ACM SIGPLAN Notices 49 (1), 179-191, 2014 | 507 | 2014 |
| A brief overview of HOL4 K Slind, M Norrish International Conference on Theorem Proving in Higher Order Logics, 28-32, 2008 | 427 | 2008 |
| C formalised in HOL M Norrish University of Cambridge, Computer Laboratory, 1998 | 289 | 1998 |
| Types, bytes, and separation logic H Tuch, G Klein, M Norrish Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2007 | 238 | 2007 |
| Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets S Bishop, M Fairbairn, M Norrish, P Sewell, M Smith, K Wansbrough Proceedings of the 2005 conference on Applications, technologies …, 2005 | 134 | 2005 |
| The PROSPER toolkit LA Dennis, G Collins, M Norrish, R Boulton, K Slind, G Robinson, ... Tools and Algorithms for the Construction and Analysis of Systems: 6th …, 2000 | 111 | 2000 |
| A new verified compiler backend for CakeML YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish Proceedings of the 21st ACM SIGPLAN International Conference on Functional …, 2016 | 100 | 2016 |
| Barendregt’s variable convention in rule inductions C Urban, S Berghofer, M Norrish Automated Deduction–CADE-21: 21st International Conference on Automated …, 2007 | 85 | 2007 |
| The verified CakeML compiler backend YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish Journal of Functional Programming 29, e2, 2019 | 81 | 2019 |
| Seed selection for successful fuzzing A Herrera, H Gunadi, S Magrath, M Norrish, M Payer, AL Hosking Proceedings of the 30th ACM SIGSOFT international symposium on software …, 2021 | 80 | 2021 |
| Learning to Reason with HOL4 tactics T Gauthier, C Kaliszyk, J Urban arXiv preprint arXiv:1804.00595, 2018 | 71* | 2018 |
| Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations S Bishop, M Fairbairn, M Norrish, P Sewell, M Smith, K Wansbrough Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of …, 2006 | 67 | 2006 |
| 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 |
| Verified characteristic formulae for CakeML A Guéneau, MO Myreen, R Kumar, M Norrish Programming Languages and Systems: 26th European Symposium on Programming …, 2017 | 57 | 2017 |
| Mechanised computability theory M Norrish Interactive Theorem Proving: Second International Conference, ITP 2011, Berg …, 2011 | 46 | 2011 |
| Verified compilation on a verified processor A Lööw, R Kumar, YK Tan, MO Myreen, M Norrish, O Abrahamsson, A Fox Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019 | 40 | 2019 |
| Recursive function definition for types with binders M Norrish International Conference on Theorem Proving in Higher Order Logics, 241-256, 2004 | 40 | 2004 |
| Verified, executable parsing A Barthwal, M Norrish Programming Languages and Systems: 18th European Symposium on Programming …, 2009 | 38 | 2009 |
| Deterministic expressions in C M Norrish European Symposium on Programming, 147-161, 1999 | 38 | 1999 |
Ramana KumarDeepMind在 cl.cam.ac.uk 的电子邮件经过验证
