Magnus Myreen

Publications

2014

Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens. CakeML: A Verified Implementation of ML. In Principles of Programming Languages (POPL), 2014.
Magnus O. Myreen, Jared Davis. The reflective Milawa theorem prover is sound (down to the machine code that runs it). In Interactive Theorem Proving (ITP), 2014.
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens. HOL with Definitions: Semantics, Soundness, and a Verified Implementation. In Interactive Theorem Proving (ITP), 2014.
Magnus O. Myreen, Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. In Journal of Functional Programming (JFP), Volume 24, Issue 2–3, 2014. (Copyright Cambridge University Press, definitive version)

2013

Thomas Sewell, Magnus O. Myreen and Gerwin Klein. Translation validation for a verified OS kernel. In Programming Language Design and Implementation (PLDI), 2013.
Magnus O. Myreen and Gregorio Curello. Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. In Certified Programs and Proofs (CPP), 2013.
Magnus O. Myreen, Scott Owens and Ramana Kumar. Steps towards verified implementations of HOL Light. In Interactive Theorem Proving (ITP), 2013.

2012

Magnus O. Myreen and Scott Owens. Proof-producing synthesis of ML from higher-order logic. In International Conference on Functional Programming (ICFP), 2012.
Magnus O. Myreen, Konrad Slind and Michael J. C. Gordon. Decompilation into Logic — Improved. In Formal Methods in Computer-Aided Design (FMCAD), 2012.
Magnus O. Myreen. Functional programs: conversions between deep and shallow embeddings. In Interactive Theorem Proving (ITP), 2012.

2011

Magnus O. Myreen and Jared Davis. A verified runtime for a verified theorem prover. In Interactive Theorem Proving (ITP), 2011.

2010

Magnus O. Myreen and Michael J. C. Gordon. Function Extraction. In Science of Computer Programming, 2010.
Magnus O. Myreen. Reusable verification of a copying collector. In Verified Software: Theories, Tools and Experiments (VSTTE), 2010.
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli and Magnus O. Myreen. x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. In Comm. ACM, 53(7), July 2010.
Anthony Fox and Magnus O. Myreen. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In Interactive Theorem Proving (ITP), 2010.
Magnus O. Myreen. Separation logic adapted for proofs by rewriting. In Interactive Theorem Proving (ITP), 2010.
Magnus O. Myreen. Verified just-in-time compiler on x86. In Principles of Programming Languages (POPL), 2010.
Anthony C. J. Fox, Michael J. C. Gordon, and Magnus O. Myreen. Specification and verification of ARM hardware and software. In David S. Hardin, editor, Design and Verification of Microprocessor Systems for High-Assurance Applications, Springer, 2010.

2009

Magnus O. Myreen and Michael J. C. Gordon. Verified LISP implementations on ARM, x86 and PowerPC. In Theorem Proving in Higher-Order Logics (TPHOLs), 2009.
Magnus O. Myreen, Konrad Slind and Michael J. C. Gordon. Extensible proof-producing compilation. In Compiler Construction (CC), 2009.
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave. The Semantics of x86-CC Multiprocessor Machine Code. In Principles of Programming Languages (POPL), 2009.
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli. The semantics of Power and ARM multiprocessor machine code. In Declarative aspects of multicore programming (DAMP), 2009.

2008

Magnus O. Myreen. Formal verification of machine-code programs. PhD dissertation, University of Cambridge, 2008.
Magnus O. Myreen, Konrad Slind and Michael J. C. Gordon. Machine-code verification for multiple architectures – An application of decompilation into logic. In Formal Methods in Computer-Aided Design (FMCAD), 2008.
Magnus O. Myreen and Michael J. C. Gordon. Transforming Programs into Recursive Functions. In the Brazilian Symposium on Formal Methods (SBMF), 2008.

2007

Magnus O. Myreen and Michael J. C. Gordon. Hoare Logic for Realistically Modelled Machine Code. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007.
Magnus O. Myreen, Anthony C. J. Fox and Michael J. C. Gordon. Hoare Logic for ARM Machine Code. In Fundamentals of Software Engineering (FSEN), 2007.
Ralph-Johan Back, Johannes Eriksson and Magnus Myreen. Testing and Verifying Invariant Based Programs in the SOCOS Environment. In Tests And Proofs (TAP), 2007.

2005

Ralph-Johan Back and Magnus Myreen. Tool Support for Invariant Based Programming. In Asia-Pacific Software Engineering Conference (APSEC), 2005.