Magnus Myreen

Magnus Myreen (myreen@chalmers.se)

Professor (in Swedish: bitr. prof.), CS, CSE, Chalmers (room 6478)

Publications

2024

Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordstrom, Andy Oertel, Yong Kiam Tan. End-to-End Verification for Subgraph Solving. To appear in AAAI Conference on Artificial Intelligence (AAAI-24), 2024.
Hrutvik Kanabar, Kacper Korban, Magnus O. Myreen. Verified Inlining and Specialisation for PureCake. To appear in European Symposium on Programming (ESOP), 2024, Springer.

2023

Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti. PureCake: A verified compiler for a lazy functional language. In Programming Language Design and Implementation (PLDI), 2023, ACM.
Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens. Cakes that bake cakes: Dynamic computation in CakeML. In Programming Language Design and Implementation (PLDI), 2023, ACM.
Oskar Abrahamsson, Magnus O. Myreen. Fast, Verified Computation for Candle. In Interactive Theorem Proving (ITP), 2023, LIPIcs.
Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen. Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML. In Journal on Software Tools for Technology Transfer (STTT), 2023, Springer.

2022

Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. Candle: A Verified Implementation of HOL Light. In Interactive Theorem Proving (ITP), 2022, LIPIcs.
Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen. Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. In Interactive Theorem Proving (ITP), 2022, LIPIcs.
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony Fox. Verified Compilation and Optimization of Floating-Point Programs in CakeML. In European Conference on Object-Oriented Programming (ECOOP), 2022, LIPIcs.
Alejandro Gomez-Londono, Magnus O. Myreen. A flat reachability-based measure for CakeML's cost semantics. To appear in the postproceedings of IFL'21, 2022, ACM.

2021

Magnus O. Myreen. The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper). In Interactive Theorem Proving (ITP), 2021.
Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. cake_lpr: Verified Propagation Redundancy Checking in CakeML. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2021.
Magnus O. Myreen. A Minimalistic Verified Bootstrapped Compiler (Proof Pearl). In Conference on Certified Programs and Proofs (CPP), 2021.

2020

Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Yong Kiam Tan. Proof-Producing Synthesis of CakeML from Monadic HOL Functions. Journal of Automated Reasoning (JAR), 2020.
Alejandro Gomez-Londono, Johannes Aman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, and Yong Kiam Tan. Do you have space for dessert? A verified space cost semantics for CakeML programs. Proc. ACM Program. Lang. (OOPSLA), 2020.

2019

Andreas Loow, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox. Verified Compilation on a Verified Processor. In Programming Language Design and Implementation (PLDI), 2019.
Johannes Aman Pohjola, Henrik Rostedt, Magnus O. Myreen. Characteristic Formulae for Liveness Properties of Non-terminating CakeML Programs. In Interactive Theorem Proving (ITP), 2019.
Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock. Icing: Supporting Fast-math Style Optimizations in a Verified Compiler. In Computer Aided Verification (CAV), 2019.
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. Journal of Functional Programming (JFP), 2019.
Adam Sandberg Ericsson, Magnus O. Myreen, and Johannes Aman Pohjola. A Verified Generational Garbage Collector for CakeML. Journal of Automated Reasoning (JAR), 2019.

2018

Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, André Platzer. VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models. In Programming Language Design and Implementation (PLDI), 2018.
Hugo Férée, Johannes Ã…man Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, and Son Ho. Program Verification in the Presence of I/O: Semantics, verified library routines, and verified applications. In Verified Software. Theories, Tools, and Experiments (VSTTE), 2018.
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan and Michael Norrish. Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. In International Joint Conference on Automated Reasoning (IJCAR), 2018.
Ramana Kumar, Eric Mullen, Zachary Tatlock and Magnus O. Myreen. Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper). In Interactive Theorem Proving (ITP), 2018.
Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony Fox. A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. In Formal Methods in Computer-Aided Design (FMCAD), 2018.

2017

Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan. Verifying Efficient Function Calls in CakeML. In International Conference on Functional Programming (ICFP), 2017.
Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola: A Verified Generational Garbage Collector for CakeML. In Interactive Theorem Proving (ITP), 2017.
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish. Verified Characteristic Formulae for CakeML. In European Symposium on Programming (ESOP), 2017.
Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar. Verified Compilation of CakeML to Multiple Machine-Code Targets. In Certified Programs and Proofs (CPP), 2017.
Oskar Abrahamsson, Magnus O. Myreen. Automatically Introducing Tail Recursion in CakeML. In Trends in Functional Programming (TFP), 2017.

2016

Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, Michael Norrish. A New Verified Compiler Backend for CakeML. In International Conference on Functional Programming (ICFP), 2016.
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens. Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation. In the Journal of Automated Reasoning (JAR), 2016.
Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan. Functional Big-step Semantics. In European Symposium on Programming (ESOP), 2016.

2015

Thomas Tuerk, Magnus O. Myreen, Ramana Kumar. Pattern Matches in HOL: A New Representation and Improved Code Generation. In Interactive Theorem Proving (ITP), 2015.
Jared Davis, Magnus O. Myreen. The self-verifying Milawa theorem prover is sound (down to the machine code that runs it). In the Journal of Automated Reasoning (JAR), 2015. (Copyright Springer, official version) bibtex

2014

Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens. CakeML: A Verified Implementation of ML. In Principles of Programming Languages (POPL), 2014. bibtex
Magnus O. Myreen, Jared Davis. The reflective Milawa theorem prover is sound (down to the machine code that runs it). In Interactive Theorem Proving (ITP), 2014. bibtex
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens. HOL with Definitions: Semantics, Soundness, and a Verified Implementation. In Interactive Theorem Proving (ITP), 2014. bibtex
Magnus O. Myreen, Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. In Journal of Functional Programming (JFP), Volume 24, Issue 2–3, 2014. (Copyright Cambridge University Press, definitive version) bibtex

2013

Thomas Sewell, Magnus O. Myreen and Gerwin Klein. Translation validation for a verified OS kernel. In Programming Language Design and Implementation (PLDI), 2013. bibtex
Magnus O. Myreen and Gregorio Curello. Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. In Certified Programs and Proofs (CPP), 2013. bibtex
Magnus O. Myreen, Scott Owens and Ramana Kumar. Steps towards verified implementations of HOL Light. In Interactive Theorem Proving (ITP), 2013. bibtex

2012

Magnus O. Myreen and Scott Owens. Proof-producing synthesis of ML from higher-order logic. In International Conference on Functional Programming (ICFP), 2012. bibtex
Magnus O. Myreen, Konrad Slind and Michael J. C. Gordon. Decompilation into Logic — Improved. In Formal Methods in Computer-Aided Design (FMCAD), 2012. bibtex
Magnus O. Myreen. Functional programs: conversions between deep and shallow embeddings. In Interactive Theorem Proving (ITP), 2012. bibtex
Magnus O. Myreen and Michael J. C. Gordon. Function Extraction. In Science of Computer Programming, 2010. bibtex

2011

Magnus O. Myreen and Jared Davis. A verified runtime for a verified theorem prover. In Interactive Theorem Proving (ITP), 2011. bibtex

2010

Magnus O. Myreen. Reusable verification of a copying collector. In Verified Software: Theories, Tools and Experiments (VSTTE), 2010. bibtex
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli and Magnus O. Myreen. x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. In Comm. ACM, 53(7), July 2010. bibtex
Anthony Fox and Magnus O. Myreen. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In Interactive Theorem Proving (ITP), 2010. bibtex
Magnus O. Myreen. Separation logic adapted for proofs by rewriting. In Interactive Theorem Proving (ITP), 2010. bibtex
Magnus O. Myreen. Verified just-in-time compiler on x86. In Principles of Programming Languages (POPL), 2010. bibtex
Anthony C. J. Fox, Michael J. C. Gordon, and Magnus O. Myreen. Specification and verification of ARM hardware and software. In David S. Hardin, editor, Design and Verification of Microprocessor Systems for High-Assurance Applications, Springer, 2010. bibtex

2009

Magnus O. Myreen and Michael J. C. Gordon. Verified LISP implementations on ARM, x86 and PowerPC. In Theorem Proving in Higher-Order Logics (TPHOLs), 2009. bibtex
Magnus O. Myreen, Konrad Slind and Michael J. C. Gordon. Extensible proof-producing compilation. In Compiler Construction (CC), 2009. bibtex
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave. The Semantics of x86-CC Multiprocessor Machine Code. In Principles of Programming Languages (POPL), 2009. bibtex
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli. The semantics of Power and ARM multiprocessor machine code. In Declarative aspects of multicore programming (DAMP), 2009. bibtex
Magnus O. Myreen and Michael J. C. Gordon. Transforming Programs into Recursive Functions. In Electron. Notes Theor. Comput. Sci., 2009. bibtex

2008

Magnus O. Myreen. Formal verification of machine-code programs. PhD dissertation, University of Cambridge, 2008. bibtex
Magnus O. Myreen, Konrad Slind and Michael J. C. Gordon. Machine-code verification for multiple architectures – An application of decompilation into logic. In Formal Methods in Computer-Aided Design (FMCAD), 2008. bibtex

2007

Magnus O. Myreen and Michael J. C. Gordon. Hoare Logic for Realistically Modelled Machine Code. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007. bibtex
Magnus O. Myreen, Anthony C. J. Fox and Michael J. C. Gordon. Hoare Logic for ARM Machine Code. In Fundamentals of Software Engineering (FSEN), 2007. bibtex
Ralph-Johan Back, Johannes Eriksson and Magnus Myreen. Testing and Verifying Invariant Based Programs in the SOCOS Environment. In Tests And Proofs (TAP), 2007. bibtex

2005

Ralph-Johan Back and Magnus Myreen. Tool Support for Invariant Based Programming. In Asia-Pacific Software Engineering Conference (APSEC), 2005. bibtex