Magnus O. Myreen

Publication Activity (10 Years)

Years Active: 2007-2024
Publications (10 Years): 42

Top Topics

Preprocessing Steps

Sparse Matrices

Top Venues

J. Autom. Reason.

Proc. ACM Program. Lang.

Publications

Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan
End-to-End Verification for Subgraph Solving. AAAI (2024)
Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel
Formally Certified Approximate Model Counting. CoRR (2024)
Hrutvik Kanabar, Kacper Korban, Magnus O. Myreen
Verified Inlining and Specialisation for PureCake. ESOP (2) (2024)
Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel
Formally Certified Approximate Model Counting. CAV (1) (2024)
Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, Jakob Nordström
Certified MaxSAT Preprocessing. IJCAR (1) (2024)
Oskar Abrahamsson, Magnus O. Myreen
Fast, Verified Computation for Candle. ITP (2023)
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
Pancake: Verified Systems Programming Made Sweeter. PLOS@SOSP (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. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Johannes Åman Pohjola, Magnus O. Myreen, Miki Tanaka
A Hoare Logic for Diverging Programs. Arch. Formal Proofs 2023 (2023)
Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML. Int. J. Softw. Tools Technol. Transf. 25 (2) (2023)
Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens
Cakes That Bake Cakes: Dynamic Computation in CakeML. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
Verified Compilation and Optimization of Floating-Point Programs in CakeML. ECOOP (2022)
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). Dagstuhl Artifacts Ser. 8 (2) (2022)
Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. ITP (2022)
Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell
Candle: A Verified Implementation of HOL Light. ITP (2022)
Magnus O. Myreen
The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper). ITP (2021)
Alejandro Gómez-Londoño, Magnus O. Myreen
A flat reachability-based measure for CakeML's cost semantics. IFL (2021)
Magnus O. Myreen
A minimalistic verified bootstrapped compiler (proof pearl). CPP (2021)
Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen
cake_lpr: Verified Propagation Redundancy Checking in CakeML. TACAS (2) (2021)
Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, Yong Kiam Tan
Do you have space for dessert? a verified space cost semantics for CakeML programs. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan
Proof-Producing Synthesis of CakeML from Monadic HOL Functions. J. Autom. Reason. 64 (7) (2020)
Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. ITP (2019)
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
The verified CakeML compiler backend. J. Funct. Program. 29 (2019)
Andreas Lööw, Magnus O. Myreen
A proof-producing translator for verilog development in HOL. FormaliSE@ICSE (2019)
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox
Verified compilation on a verified processor. PLDI (2019)
Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock
Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler. CAV (2) (2019)
Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola
A Verified Generational Garbage Collector for CakeML. J. Autom. Reason. 63 (2) (2019)
Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, André Platzer
VeriPhy: verified controller executables from verified cyber-physical system models. PLDI (2018)
Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. FMCAD (2018)
Ramana Kumar, Magnus O. Myreen
Clocked Definitions in HOL. CoRR (2018)
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. IJCAR (2018)
Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho
Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications. VSTTE (2018)
Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). ITP (2018)
Heiko Becker, Eva Darulova, Magnus O. Myreen
A Verified Certificate Checker for Floating-Point Error Bounds. CoRR (2017)
Oskar Abrahamsson, Magnus O. Myreen
Automatically Introducing Tail Recursion in CakeML. TFP (2017)
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish
Verified Characteristic Formulae for CakeML. ESOP (2017)
Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar
Verified compilation of CakeML to multiple machine-code targets. CPP (2017)
Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola
A Verified Generational Garbage Collector for CakeML. ITP (2017)
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan
Verifying efficient function calls in CakeML. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
A new verified compiler backend for CakeML. ICFP (2016)
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens
Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation. J. Autom. Reason. 56 (3) (2016)
Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan
Functional Big-Step Semantics. ESOP (2016)
Jared Davis, Magnus O. Myreen
The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it). J. Autom. Reason. 55 (2) (2015)
Thomas Tuerk, Magnus O. Myreen, Ramana Kumar
Pattern Matches in HOL: - A New Representation and Improved Code Generation. ITP (2015)
Magnus O. Myreen, Scott Owens
Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24 (2-3) (2014)
Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens
CakeML: a verified implementation of ML. POPL (2014)
Magnus O. Myreen, Jared Davis
The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It). ITP (2014)
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens
HOL with Definitions: Semantics, Soundness, and a Verified Implementation. ITP (2014)
Magnus O. Myreen, Gregorio Curello
Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. CPP (2013)
Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein
Translation validation for a verified OS kernel. PLDI (2013)
Magnus O. Myreen, Scott Owens, Ramana Kumar
Steps towards Verified Implementations of HOL Light. ITP (2013)
Magnus O. Myreen, Scott Owens
Proof-producing synthesis of ML from higher-order logic. ICFP (2012)
Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind
Decompilation into logic - Improved. FMCAD (2012)
Magnus O. Myreen
Functional Programs: Conversions between Deep and Shallow Embeddings. ITP (2012)
Magnus O. Myreen, Michael J. C. Gordon
Function extraction. Sci. Comput. Program. 77 (4) (2012)
Magnus O. Myreen, Jared Davis
A Verified Runtime for a Verified Theorem Prover. ITP (2011)
Anthony C. J. Fox, Magnus O. Myreen
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. ITP (2010)
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen
x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Commun. ACM 53 (7) (2010)
Magnus O. Myreen
Separation Logic Adapted for Proofs by Rewriting. ITP (2010)
Magnus O. Myreen
Verified just-in-time compiler on x86. POPL (2010)
Magnus O. Myreen
Reusable Verification of a Copying Collector. VSTTE (2010)
Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon
Extensible Proof-Producing Compilation. CC (2009)
Magnus O. Myreen, Michael J. C. Gordon
Verified LISP Implementations on ARM, x86 and PowerPC. TPHOLs (2009)
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. DAMP (2009)
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. POPL (2009)
Magnus O. Myreen, Michael J. C. Gordon
Transforming Programs into Recursive Functions. Electron. Notes Theor. Comput. Sci. 240 (2009)
Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind
Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. FMCAD (2008)
Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon
Hoare Logic for ARM Machine Code. FSEN (2007)
Magnus O. Myreen, Michael J. C. Gordon
Hoare Logic for Realistically Modelled Machine Code. TACAS (2007)