Front page
Research:
• Decompilation
• Synthesis
• Lisp and ML
• Verified stacks
Teaching
Biography
Publications

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

Royal Society University Research Fellow,
Computer Laboratory, University of Cambridge

Recent activity

Aug 2013 — CPP'13 has accepted my paper on a verified bignum arithmetic library.

Apr 2013 — I've been invited to give a tutorial at LOLA'13.

Mar 2013 — ITP'13 has accepted our paper on Steps Towards Verified Implementations of HOL Light, co-authors: Scott Owens and Ramana Kumar.

Feb 2013 — PLDI'13 has accepted a paper describing my collaboration with the L4.verified project, co-authors: Thomas Sewell and Gerwin Klein.

Dec 2012 — had the pleasure of meeting Carroll Morgan, author of one of my favourite books on program construction: Programming from Specifications.

Dec 2012 — arrived at NICTA for a 10-week visit to the L4.verified team

Oct 2012 — became a Royal Society Research Fellow.

My research focuses on program verification, interactive theorem proving and, particularly, the challenges of making interactive proofs more automatic / scale to real code. This webpage provides a brief introduction to my research in the following areas:

Decompilation into logic — verification of machine code
Proof-producing synthesis from logic
Verified Lisp and ML runtimes
Connecting things up: verified stacks

Send me an email if you'd like to know more. My email address is at the top of the page.