Magnus O. Myreen

85 papers A* 8A 9B 26C 1Journal 24Unranked 15
YearRankTypeTitle / Venue / Authors
2026 C conf
A One-Pass CPS Transform with Simulation on the Nose.
PADL
Pascal Y. Lasnier, Jeremy Yallop, Magnus O. Myreen
2026 B conf
Brack: A Verified Compiler for Scheme via CakeML.
CPP
Pascal Y. Lasnier, Jeremy Yallop, Magnus O. Myreen
2026 A* conf
Faster Certified Symmetry Breaking Using Orders with Auxiliary Variables.
AAAI
Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, Yong Kiam Tan
2026 B conf
Verified VCG and Verified Compiler for Dafny.
CPP
Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan
2025 J jnl
Candle: A Verified Implementation of HOL Light (Extended Version).
J. Autom. Reason.
Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell
2025 A conf
Efficient Certified Reasoning for Binarized Neural Networks.
SAT
Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel
2025 J jnl
Efficient Certified Reasoning for Binarized Neural Networks.
CoRR
Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel
2025 J jnl
Fast, Verified Computation for HOL ITPs.
J. Autom. Reason.
Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Hrutvik Kanabar, Johannes Åman Pohjola
2025 J jnl
Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables.
CoRR
Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, Yong Kiam Tan
2025 B conf
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life.
ITP
Magnus O. Myreen, Mario Carneiro
2025 J jnl
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life.
CoRR
Magnus O. Myreen, Mario Carneiro
2025 A conf
Practically Feasible Proof Logging for Pseudo-Boolean Optimization.
CP
Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, Marc Vinyals
2025 J jnl
Verified VCG and Verified Compiler for Dafny.
CoRR
Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan
2024 — conf
Certified MaxSAT Preprocessing.
IJCAR (1)
Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, Jakob Nordström
2024 A* conf
End-to-End Verification for Subgraph Solving.
AAAI
Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan
2024 — conf
Formally Certified Approximate Model Counting.
CAV (1)
Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel
2024 J jnl
Formally Certified Approximate Model Counting.
CoRR
Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel
2024 — conf
Verified Inlining and Specialisation for PureCake.
ESOP (2)
Hrutvik Kanabar, Kacper Korban, Magnus O. Myreen
2023 J jnl
A Hoare Logic for Diverging Programs.
Arch. Formal Proofs
Johannes Åman Pohjola, Magnus O. Myreen, Miki Tanaka
2023 J jnl
Cakes That Bake Cakes: Dynamic Computation in CakeML.
Proc. ACM Program. Lang.
Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens
2023 B conf
Fast, Verified Computation for Candle.
ITP
Oskar Abrahamsson, Magnus O. Myreen
2023 — conf
Pancake: Verified Systems Programming Made Sweeter.
PLOS@SOSP
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
2023 J jnl
PureCake: A Verified Compiler for a Lazy Functional Language.
Proc. ACM Program. Lang.
Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti
2023 J jnl
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML.
Int. J. Softw. Tools Technol. Transf.
Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen
2022 B conf
Candle: A Verified Implementation of HOL Light.
ITP
Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell
2022 B conf
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification.
ITP
Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen
2022 J jnl
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact).
Dagstuhl Artifacts Ser.
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
2022 A conf
Verified Compilation and Optimization of Floating-Point Programs in CakeML.
ECOOP
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
2021 — conf
A flat reachability-based measure for CakeML's cost semantics.
IFL
Alejandro Gómez-Londoño, Magnus O. Myreen
2021 B conf
A minimalistic verified bootstrapped compiler (proof pearl).
CPP
Magnus O. Myreen
2021 B conf
The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper).
ITP
Magnus O. Myreen
2021 — conf
cake_lpr: Verified Propagation Redundancy Checking in CakeML.
TACAS (2)
Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen
2020 J jnl
Do you have space for dessert? a verified space cost semantics for CakeML programs.
Proc. ACM Program. Lang.
Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, Yong Kiam Tan
2020 J jnl
Proof-Producing Synthesis of CakeML from Monadic HOL Functions.
J. Autom. Reason.
Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan
2019 J jnl
A Verified Generational Garbage Collector for CakeML.
J. Autom. Reason.
Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola
2019 — conf
A proof-producing translator for verilog development in HOL.
FormaliSE@ICSE
Andreas Lööw, Magnus O. Myreen
2019 B conf
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs.
ITP
Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen
2019 — conf
Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler.
CAV (2)
Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock
2019 B ed.
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019
CPP
Assia Mahboubi, Magnus O. Myreen
2019 J jnl
The verified CakeML compiler backend.
J. Funct. Program.
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
2019 — ed.
Trends in Functional Programming - 19th International Symposium, TFP 2018, Gothenburg, Sweden, June 11-13, 2018, Revised Selected Papers
TFP
Michal H. Palka, Magnus O. Myreen
2019 A* conf
Verified compilation on a verified processor.
PLDI
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox
2018 B conf
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4.
FMCAD
Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox
2018 J jnl
Clocked Definitions in HOL.
CoRR
Ramana Kumar, Magnus O. Myreen
2018 — conf
Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications.
VSTTE
Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho
2018 A conf
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.
IJCAR
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish
2018 B conf
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper).
ITP
Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen
2018 A* conf
VeriPhy: verified controller executables from verified cyber-physical system models.
PLDI
Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, André Platzer
2017 J jnl
A Verified Certificate Checker for Floating-Point Error Bounds.
CoRR
Heiko Becker, Eva Darulova, Magnus O. Myreen
2017 B conf
A Verified Generational Garbage Collector for CakeML.
ITP
Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola
2017 — conf
Automatically Introducing Tail Recursion in CakeML.
TFP
Oskar Abrahamsson, Magnus O. Myreen
2017 A conf
Verified Characteristic Formulae for CakeML.
ESOP
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish
2017 B conf
Verified compilation of CakeML to multiple machine-code targets.
CPP
Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar
2017 J jnl
Verifying efficient function calls in CakeML.
Proc. ACM Program. Lang.
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan
2016 A conf
A new verified compiler backend for CakeML.
ICFP
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
2016 A conf
Functional Big-Step Semantics.
ESOP
Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan
2016 J jnl
Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation.
J. Autom. Reason.
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens
2015 B conf
Pattern Matches in HOL: - A New Representation and Improved Code Generation.
ITP
Thomas Tuerk, Magnus O. Myreen, Ramana Kumar
2015 J jnl
The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it).
J. Autom. Reason.
Jared Davis, Magnus O. Myreen
2014 A* conf
CakeML: a verified implementation of ML.
POPL
Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens
2014 B conf
HOL with Definitions: Semantics, Soundness, and a Verified Implementation.
ITP
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens
2014 J jnl
Proof-producing translation of higher-order logic into pure and stateful ML.
J. Funct. Program.
Magnus O. Myreen, Scott Owens
2014 B conf
The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It).
ITP
Magnus O. Myreen, Jared Davis
2013 B conf
Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code.
CPP
Magnus O. Myreen, Gregorio Curello
2013 B conf
Steps towards Verified Implementations of HOL Light.
ITP
Magnus O. Myreen, Scott Owens, Ramana Kumar
2013 A* conf
Translation validation for a verified OS kernel.
PLDI
Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein
2012 B conf
Decompilation into logic - Improved.
FMCAD
Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind
2012 J jnl
Function extraction.
Sci. Comput. Program.
Magnus O. Myreen, Michael J. C. Gordon
2012 B conf
Functional Programs: Conversions between Deep and Shallow Embeddings.
ITP
Magnus O. Myreen
2012 A conf
Proof-producing synthesis of ML from higher-order logic.
ICFP
Magnus O. Myreen, Scott Owens
2011 B conf
A Verified Runtime for a Verified Theorem Prover.
ITP
Magnus O. Myreen, Jared Davis
2010 B conf
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture.
ITP
Anthony C. J. Fox, Magnus O. Myreen
2010 — conf
Reusable Verification of a Copying Collector.
VSTTE
Magnus O. Myreen
2010 B conf
Separation Logic Adapted for Proofs by Rewriting.
ITP
Magnus O. Myreen
2010 — ch.
Specification and Verification of ARM Hardware and Software.
Design and Verification of Microprocessor Systems for High-Assurance Applications
Anthony C. J. Fox, Michael J. C. Gordon, Magnus O. Myreen
2010 A* conf
Verified just-in-time compiler on x86.
POPL
Magnus O. Myreen
2010 J jnl
x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors.
Commun. ACM
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen
2009 B conf
Extensible Proof-Producing Compilation.
CC
Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon
2009 — conf
The semantics of power and ARM multiprocessor machine code.
DAMP
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli
2009 A* conf
The semantics of x86-CC multiprocessor machine code.
POPL
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave
2009 — conf
Verified LISP Implementations on ARM, x86 and PowerPC.
TPHOLs
Magnus O. Myreen, Michael J. C. Gordon
2008 B conf
Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic.
FMCAD
Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind
2008 — conf
Transforming Programs into Recursive Functions.
SBMF
Magnus O. Myreen, Michael J. C. Gordon
2007 — conf
Hoare Logic for ARM Machine Code.
FSEN
Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon
2007 A conf
Hoare Logic for Realistically Modelled Machine Code.
TACAS
Magnus O. Myreen, Michael J. C. Gordon