Magnus Myreen
Recent activity

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.

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.

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.