Magnus Myreen
Magnus Myreen
Chalmers University of Technology
Verified email at - Homepage
Cited by
Cited by
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
CakeML: A Verified Implementation of ML
R Kumar, MO Myreen, SA Owens, M Norrish
ACM Symposium on Principles of Programming Languages (POPL) 2014, 0
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
A trustworthy monadic formalization of the ARMv7 instruction set architecture
A Fox, MO Myreen
Interactive Theorem Proving: First International Conference, ITP 2010 …, 2010
Translation validation for a verified OS kernel
TAL Sewell, MO Myreen, G Klein
Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013
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
Functional big-step semantics
S Owens, MO Myreen, R Kumar, YK Tan
Programming Languages and Systems: 25th European Symposium on Programming …, 2016
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
Verified just-in-time compiler on x86
MO Myreen
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010
Hoare logic for realistically modelled machine code
MO Myreen, MJC Gordon
Tools and Algorithms for the Construction and Analysis of Systems: 13th …, 2007
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
VeriPhy: verified controller executables from verified cyber-physical system models
B Bohrer, YK Tan, S Mitsch, MO Myreen, A Platzer
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language …, 2018
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
Formal verification of machine-code programs
MO Myreen
British Computer Society, 2011
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
The verified CakeML compiler backend
YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish
Journal of Functional Programming 29, e2, 2019
Decompilation into logic—improved
MO Myreen, MJC Gordon, K Slind
2012 Formal Methods in Computer-Aided Design (FMCAD), 78-81, 2012
Verified characteristic formulae for CakeML
A Guéneau, MO Myreen, R Kumar, M Norrish
European Symposium on Programming (ESOP), Springer, Lecture Notes in …, 2017
A verified runtime for a verified theorem prover
MO Myreen, J Davis
Interactive Theorem Proving: Second International Conference, ITP 2011, Berg …, 2011
HOL with Definitions: Semantics, Soundness, and a Verified Implementation
R Kumar, R Arthan, MO Myreen, S Owens
Interactive Theorem Proving: Fifth International Conference, ITP 2014, 2014
The system can't perform the operation now. Try again later.
Articles 1–20