Magnus Myreen

Magnus.Myreen (

former Royal Society University Research Fellow, CL, Cambridge
but nowadays at Chalmers
Recent activity

My recent activity is listed
on my Chalmers page.

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.