Magnus Myreen
Recent activity

Jul 2014 — took part in the Vienna Summer of Logic meeting, where I gave an invited talk at ACL2'14, and talks at the HOL'14 and QED+20 workshop; and presented a paper at ITP'14.

Jul 2014 — took part in workshop Certification of high-level and low-level programs.

Apr 2014ITP'14 accepted two submissions where I'm co-author: The reflective Milawa theorem prover is sound (down to the machine code that runs it) and HOL with Definitions: Semantics, Soundness, and a Verified Implementation.

Jan 2014 — my co-author Ramana presented our latest work on CakeML at POPL'14.

Oct 2013 — lecturing a new course on formal methods and functional programming.

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

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.