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

New! Anthony Fox and Magnus O. Myreen. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. To appear in Interactive Theorem Proving (ITP), 2010.

New! Magnus O. Myreen. Separation logic adapted for proofs by rewriting. To appear in Interactive Theorem Proving (ITP), 2010.

New! Magnus O. Myreen. Verified just-in-time compiler on x86. In Principles of Programming Languages (POPL), 2010.

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

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.

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.

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 and Magnus Myreen. Tool Support for Invariant Based Programming. In Asia-Pacific Software Engineering Conference (APSEC), 2005.