Magnus Myreen
University of Cambridge
|
I am an RA in the Automated Reasoning Group at the Computer Laboratory in Cambridge, working with Mike Gordon. Papers:
I've written a beginner's guide to HOL: Guide to HOL4 interaction and basic proofsMagnus O. Myreen, Konrad Slind and Michael J. C. Gordon.
Extensible proof-producing compilation.
To appear in Proceedings of 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 Proceedings of 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.
Proceedings of Formal Methods in Computer-Aided Design (FMCAD), 2008.Magnus O. Myreen and Michael J. C. Gordon.
Transforming Programs into Recursive Functions.
Proceedings of the Brazilian Symposium on Formal Methods (SBMF), 2008.Magnus O. Myreen and Michael J. C. Gordon.
Hoare Logic for Realistically Modelled Machine Code.
Proceedings of 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.
Proceedings of the IPM International Symposium on Fundamentals of Software Engineering (FSEN), 2007.Ralph-Johan Back and Magnus Myreen.
Tool Support for Invariant Based Programming.
Proceedings of the Asia-Pacific Software Engineering Conference (APSEC), 2005.
During the summers of 2004 and 2005 I worked on a verification condition generator at Åbo Akademi (TUCS), where Ralph-Johan Back supervised me.