Magnus O. Myreen

According to our database, Magnus O. Myreen authored at least 70 papers between 2005 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

Certified MaxSAT Preprocessing.

Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, Jakob Nordström

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

Verified Inlining and Specialisation for PureCake.

Hrutvik Kanabar, Kacper Korban, Magnus O. Myreen

Proceedings of the Programming Languages and Systems, 2024

Formally Certified Approximate Model Counting.

Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

End-to-End Verification for Subgraph Solving.

Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan

Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

2023

Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML.

Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen

Int. J. Softw. Tools Technol. Transf., April, 2023

Cakes That Bake Cakes: Dynamic Computation in CakeML.

Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens

Proc. ACM Program. Lang., 2023

PureCake: A Verified Compiler for a Lazy Functional Language.

Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti

Proc. ACM Program. Lang., 2023

A Hoare Logic for Diverging Programs.

Johannes Åman Pohjola, Magnus O. Myreen, Miki Tanaka

Arch. Formal Proofs, 2023

Pancake: Verified Systems Programming Made Sweeter.

Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Tsun Wang Sau, Benjamin Nott, Tiana J. Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus O. Myreen, Michael Norrish, Gernot Heiser

Proceedings of the 12th Workshop on Programming Languages and Operating Systems, 2023

Fast, Verified Computation for Candle.

Oskar Abrahamsson, Magnus O. Myreen

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2022

Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact).

Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox

Dagstuhl Artifacts Ser., 2022

Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification.

Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Candle: A Verified Implementation of HOL Light.

Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Verified Compilation and Optimization of Floating-Point Programs in CakeML.

Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox

Proceedings of the 36th European Conference on Object-Oriented Programming, 2022

2021

cake_lpr: Verified Propagation Redundancy Checking in CakeML.

Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper).

Magnus O. Myreen

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

A flat reachability-based measure for CakeML's cost semantics.

Alejandro Gómez-Londoño, Magnus O. Myreen

Proceedings of the 33rd Symposium on Implementation and Application of Functional Languages, 2021

A minimalistic verified bootstrapped compiler (proof pearl).

Magnus O. Myreen

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

Do you have space for dessert? a verified space cost semantics for CakeML programs.

Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, Yong Kiam Tan

Proc. ACM Program. Lang., 2020

Proof-Producing Synthesis of CakeML from Monadic HOL Functions.

Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan

J. Autom. Reason., 2020

2019

The verified CakeML compiler backend.

Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish

J. Funct. Program., 2019

A Verified Generational Garbage Collector for CakeML.

Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola

J. Autom. Reason., 2019

Verified compilation on a verified processor.

Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs.

Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

A proof-producing translator for verilog development in HOL.

Andreas Lööw, Magnus O. Myreen

Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, 2019

Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler.

Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

Clocked Definitions in HOL.

Ramana Kumar, Magnus O. Myreen

CoRR, 2018

Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications.

Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

VeriPhy: verified controller executables from verified cyber-physical system models.

Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, André Platzer

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper).

Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4.

Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.

Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Verifying efficient function calls in CakeML.

Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan

Proc. ACM Program. Lang., 2017

A Verified Certificate Checker for Floating-Point Error Bounds.

Heiko Becker, Eva Darulova, Magnus O. Myreen

CoRR, 2017

Automatically Introducing Tail Recursion in CakeML.

Oskar Abrahamsson, Magnus O. Myreen

Proceedings of the Trends in Functional Programming - 18th International Symposium, 2017

Verified Characteristic Formulae for CakeML.

Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish

Proceedings of the Programming Languages and Systems, 2017

Verified compilation of CakeML to multiple machine-code targets.

Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation.

Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens

J. Autom. Reason., 2016

A new verified compiler backend for CakeML.

Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Functional Big-Step Semantics.

Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan

Proceedings of the Programming Languages and Systems, 2016

2015

The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it).

Jared Davis, Magnus O. Myreen

J. Autom. Reason., 2015

Pattern Matches in HOL: - A New Representation and Improved Code Generation.

Thomas Tuerk, Magnus O. Myreen, Ramana Kumar

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014

Proof-producing translation of higher-order logic into pure and stateful ML.

Magnus O. Myreen, Scott Owens

J. Funct. Program., 2014

CakeML: a verified implementation of ML.

Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

HOL with Definitions: Semantics, Soundness, and a Verified Implementation.

Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

Translation validation for a verified OS kernel.

Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

Steps towards Verified Implementations of HOL Light.

Magnus O. Myreen, Scott Owens, Ramana Kumar

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code.

Magnus O. Myreen, Gregorio Curello

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

Function extraction.

Magnus O. Myreen, Michael J. C. Gordon

Sci. Comput. Program., 2012

Functional Programs: Conversions between Deep and Shallow Embeddings.

Magnus O. Myreen

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Proof-producing synthesis of ML from higher-order logic.

Magnus O. Myreen, Scott Owens

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

Decompilation into logic - Improved.

Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind

Proceedings of the Formal Methods in Computer-Aided Design, 2012

2011

A Verified Runtime for a Verified Theorem Prover.

Magnus O. Myreen, Jared Davis

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010

x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors.

Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen

Commun. ACM, 2010

Reusable Verification of a Copying Collector.

Magnus O. Myreen

Proceedings of the Verified Software: Theories, 2010

Verified just-in-time compiler on x86.

Magnus O. Myreen

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Separation Logic Adapted for Proofs by Rewriting.

Magnus O. Myreen

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture.

Anthony C. J. Fox, Magnus O. Myreen

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Specification and Verification of ARM Hardware and Software.

Anthony C. J. Fox, Michael J. C. Gordon, Magnus O. Myreen

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009

Formal verification of machine-code programs.

Magnus Oskar Myreen

PhD thesis, 2009

Verified LISP Implementations on ARM, x86 and PowerPC.

Magnus O. Myreen, Michael J. C. Gordon

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

The semantics of x86-CC multiprocessor machine code.

Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

The semantics of power and ARM multiprocessor machine code.

Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli

Proceedings of the POPL 2009 Workshop on Declarative Aspects of Multicore Programming, 2009

Extensible Proof-Producing Compilation.

Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon

Proceedings of the Compiler Construction, 18th International Conference, 2009

2008

Transforming Programs into Recursive Functions.

Magnus O. Myreen, Michael J. C. Gordon

Proceedings of the Eleventh Brazilian Symposium on Formal Methods, 2008

Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic.

Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind

Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007

Testing and Verifying Invariant Based Programs in the SOCOS Environment.

Ralph-Johan Back, Johannes Eriksson, Magnus Myreen

Proceedings of the Tests and Proofs - 1st International Conference, 2007

Hoare Logic for Realistically Modelled Machine Code.

Magnus O. Myreen, Michael J. C. Gordon

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Hoare Logic for ARM Machine Code.

Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon

Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

2005

Tool Support for Invariant Based Programming.

Ralph-Johan Back, Magnus Myreen

Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), 2005