Magnus Myreen
Recent activity

Apr 2015 — taking part in a Dagstuhl seminar on Qualification of FM Tools by Darren Cofer, Gerwin Klein, Konrad Slind, Virginie Wiels.

Mar 2015 — submitted two papers to ITP'15 which is organised by Christian Urban and Xingyuan Zhang this year.

Feb 2015 — the Journal of Automated Reasoning (JAR) has accepted our paper on the Milawa/Jitawa work. Paper appearing here soon...

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.



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.