Magnus.Myreen (@cl.cam.ac.uk)
Royal Society Research Fellow,Computer Laboratory, University of Cambridge
My PhD dissertation was selected as the winner of the BCS Distinguished Dissertation Competition 2010.
Publications
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.