Magnus Myreen

Magnus.Myreen (@cl.cam.ac.uk)

Royal Society University Research Fellow, CL, Cambridge
but nowadays at Chalmers

Publications

2015

Thomas Tuerk, Magnus O. Myreen, Ramana Kumar. Pattern Matches in HOL: A New Representation and Improved Code Generation. In Interactive Theorem Proving (ITP), 2015. To appear
Jared Davis, Magnus O. Myreen. The self-verifying Milawa theorem prover is sound (down to the machine code that runs it). In the Journal of Automated Reasoning (JAR), 2015. (Copyright Springer, official version) bibtex

2014

Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens. CakeML: A Verified Implementation of ML. In Principles of Programming Languages (POPL), 2014. bibtex
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. bibtex
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens. HOL with Definitions: Semantics, Soundness, and a Verified Implementation. In Interactive Theorem Proving (ITP), 2014. bibtex
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) bibtex

2013

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

2012

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

2011

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

2010

Magnus O. Myreen. Reusable verification of a copying collector. In Verified Software: Theories, Tools and Experiments (VSTTE), 2010. bibtex
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. bibtex
Anthony Fox and Magnus O. Myreen. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In Interactive Theorem Proving (ITP), 2010. bibtex
Magnus O. Myreen. Separation logic adapted for proofs by rewriting. In Interactive Theorem Proving (ITP), 2010. bibtex
Magnus O. Myreen. Verified just-in-time compiler on x86. In Principles of Programming Languages (POPL), 2010. bibtex
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. bibtex

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. bibtex
Magnus O. Myreen, Konrad Slind and Michael J. C. Gordon. Extensible proof-producing compilation. In Compiler Construction (CC), 2009. bibtex
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. bibtex
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. bibtex
Magnus O. Myreen and Michael J. C. Gordon. Transforming Programs into Recursive Functions. In Electron. Notes Theor. Comput. Sci., 2009. bibtex

2008

Magnus O. Myreen. Formal verification of machine-code programs. PhD dissertation, University of Cambridge, 2008. bibtex
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. bibtex

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. bibtex
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. bibtex
Ralph-Johan Back, Johannes Eriksson and Magnus Myreen. Testing and Verifying Invariant Based Programs in the SOCOS Environment. In Tests And Proofs (TAP), 2007. bibtex

2005

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