| x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors P Sewell, S Sarkar, S Owens, FZ Nardelli, MO Myreen Communications of the ACM 53 (7), 89-97, 2010 | 561 | 2010 |
| CakeML: A Verified Implementation of ML R Kumar, MO Myreen, SA Owens, M Norrish ACM Symposium on Principles of Programming Languages (POPL) 2014, 0 | 518* | |
| The semantics of x86-CC multiprocessor machine code S Sarkar, P Sewell, FZ Nardelli, S Owens, T Ridge, T Braibant, ... ACM SIGPLAN Notices 44 (1), 379-391, 2009 | 210 | 2009 |
| Translation validation for a verified OS kernel TAL Sewell, MO Myreen, G Klein Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013 | 209 | 2013 |
| A trustworthy monadic formalization of the ARMv7 instruction set architecture A Fox, MO Myreen International Conference on Interactive Theorem Proving, 243-258, 2010 | 195 | 2010 |
| The semantics of Power and ARM multiprocessor machine code J Alglave, A Fox, S Ishtiaq, MO Myreen, S Sarkar, P Sewell, FZ Nardelli Proceedings of the 4th workshop on Declarative aspects of multicore …, 2009 | 147 | 2009 |
| Functional big-step semantics S Owens, MO Myreen, R Kumar, YK Tan Programming Languages and Systems: 25th European Symposium on Programming …, 2016 | 119 | 2016 |
| VeriPhy: verified controller executables from verified cyber-physical system models R Bohrer, YK Tan, S Mitsch, MO Myreen, A Platzer Proceedings of the 39th ACM SIGPLAN Conference on Programming Language …, 2018 | 97 | 2018 |
| 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 | 97 | 2016 |
| Verified just-in-time compiler on x86 MO Myreen Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010 | 96 | 2010 |
| Hoare logic for realistically modelled machine code MO Myreen, MJC Gordon International Conference on Tools and Algorithms for the Construction and …, 2007 | 92 | 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 | 86 | 2019 |
| Machine-code verification for multiple architectures-an application of decompilation into logic MO Myreen, MJC Gordon, K Slind 2008 Formal Methods in Computer-Aided Design, 1-8, 2008 | 82 | 2008 |
| Proof-producing translation of higher-order logic into pure and stateful ML MO Myreen, S Owens Journal of Functional Programming 24 (2-3), 284-315, 2014 | 77 | 2014 |
| Self-formalisation of higher-order logic: Semantics, soundness, and a verified implementation R Kumar, R Arthan, MO Myreen, S Owens Journal of Automated Reasoning 56, 221-259, 2016 | 68 | 2016 |
| Formal verification of machine-code programs MO Myreen British Computer Society, 2011 | 60 | 2011 |
| Verified characteristic formulae for CakeML A Guéneau, MO Myreen, R Kumar, M Norrish European Symposium on Programming (ESOP), Springer, Lecture Notes in …, 2017 | 58 | 2017 |
| Decompilation into logic—improved MO Myreen, MJC Gordon, K Slind 2012 Formal Methods in Computer-Aided Design (FMCAD), 78-81, 2012 | 52 | 2012 |
| Proof-producing synthesis of ML from higher-order logic MO Myreen, S Owens ACM SIGPLAN Notices 47 (9), 115-126, 2012 | 48 | 2012 |
| A verified runtime for a verified theorem prover MO Myreen, J Davis International Conference on Interactive Theorem Proving, 265-280, 2011 | 43 | 2011 |
Ramana KumarDeepMind在 cl.cam.ac.uk 的电子邮件经过验证
