Magnus Myreen PhD student. University of Cambridge Computer Laboratory @ Email: magnus.myreen cl.cam.ac.uk

I am a final-year PhD student in the Automated Reasoning Group at the Computer Laboratory in Cambridge.
Mike Gordon and Matthew Parkinson supervise my PhD work, which centres around verification of
machine-code programs. Papers:

Magnus O. Myreen and Michael J. C. Gordon.
Hoare Logic for Realistically Modelled Machine Code. bib.
Proceedings of the 13th International Conference on 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. bib.
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. bib.
Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC), 2005.

I've written a beginner's guide to HOL: Guide to HOL4 interaction and basic proofs

During the summers of 2004 and 2005 I worked on a verification condition generator at Åbo Akademi (TUCS),
where Ralph-Johan Back supervised me.