Magnus O. Myreen
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
52
Venues
19
Active years
2007–2026
Best venue rank
A*
Where they publish
Papers
52 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | AAAI | Faster Certified Symmetry Breaking Using Orders with Auxiliary Variables. | Markus Anders, Bart Bogaerts, Benjamin Bog, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordstrm, Andy Oertel, Adrian Rebola-Pardo, Yong Kiam Tan |
| 2026 | CP | End-to-End Certified Graph Colouring. | Simon Dold, George Katsirelos, Wietze Koops, Magnus O. Myreen, Jakob Nordstrm, Andy Oertel, Yong Kiam Tan |
| 2026 | CPP | Brack: A Verified Compiler for Scheme via CakeML. | Pascal Y. Lasnier, Jeremy Yallop, Magnus O. Myreen |
| 2026 | CPP | Verified VCG and Verified Compiler for Dafny. | Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan |
| 2026 | PADL | A One-Pass CPS Transform with Simulation on the Nose. | Pascal Y. Lasnier, Jeremy Yallop, Magnus O. Myreen |
| 2025 | CP | Practically Feasible Proof Logging for Pseudo-Boolean Optimization. | Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordstrm, Andy Oertel, Yong Kiam Tan, Marc Vinyals |
| 2025 | ITP | GOL in GOL in HOL: Verified Circuits in Conway's Game of Life. | Magnus O. Myreen, Mario Carneiro |
| 2025 | SAT | Efficient Certified Reasoning for Binarized Neural Networks. | Jiong Yang, Yong Kiam Tan, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel |
| 2024 | AAAI | End-to-End Verification for Subgraph Solving. | Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordstrm, Andy Oertel, Yong Kiam Tan |
| 2024 | CAV | Formally Certified Approximate Model Counting. | Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, Kuldeep S. Meel |
| 2024 | ESOP | Verified Inlining and Specialisation for PureCake. | Hrutvik Kanabar, Kacper Korban, Magnus O. Myreen |
| 2024 | IJCAR | Certified MaxSAT Preprocessing. | Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Jrvisalo, Magnus O. Myreen, Jakob Nordstrm |
| 2023 | ITP | Fast, Verified Computation for Candle. | Oskar Abrahamsson, Magnus O. Myreen |
| 2023 | PLOS | 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 |
| 2022 | ECOOP | 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 |
| 2022 | ITP | Candle: A Verified Implementation of HOL Light. | Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, Thomas Sewell |
| 2022 | ITP | Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. | Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen |
| 2021 | CPP | A minimalistic verified bootstrapped compiler (proof pearl). | Magnus O. Myreen |
| 2021 | ITP | The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper). | Magnus O. Myreen |
| 2021 | TACAS | cake_lpr: Verified Propagation Redundancy Checking in CakeML. | Yong Kiam Tan, Marijn J. H. Heule, Magnus O. Myreen |
| 2019 | CAV | Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler. | Heiko Becker, Eva Darulova, Magnus O. Myreen, Zachary Tatlock |
| 2019 | ICSE | A proof-producing translator for verilog development in HOL. | Andreas Lw, Magnus O. Myreen |
| 2019 | ITP | Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. | Johannes man Pohjola, Henrik Rostedt, Magnus O. Myreen |
| 2019 | PLDI | Verified compilation on a verified processor. | Andreas Lw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox |
| 2018 | CADE | 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 |
| 2018 | FMCAD | A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. | Heiko Becker, Nikita Zyuzin, Raphal Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox |
| 2018 | ITP | Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper). | Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen |
| 2018 | PLDI | VeriPhy: verified controller executables from verified cyber-physical system models. | Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, Andr Platzer |
| 2017 | CPP | Verified compilation of CakeML to multiple machine-code targets. | Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar |
| 2017 | ESOP | Verified Characteristic Formulae for CakeML. | Armal Guneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish |
| 2017 | ITP | A Verified Generational Garbage Collector for CakeML. | Adam Sandberg Ericsson, Magnus O. Myreen, Johannes man Pohjola |
| 2016 | ESOP | Functional Big-Step Semantics. | Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan |
| 2016 | ICFP | A new verified compiler backend for CakeML. | Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish |
| 2015 | ITP | Pattern Matches in HOL: - A New Representation and Improved Code Generation. | Thomas Tuerk, Magnus O. Myreen, Ramana Kumar |
| 2014 | ITP | HOL with Definitions: Semantics, Soundness, and a Verified Implementation. | Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens |
| 2014 | ITP | The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It). | Magnus O. Myreen, Jared Davis |
| 2014 | POPL | CakeML: a verified implementation of ML. | Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens |
| 2013 | CPP | Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. | Magnus O. Myreen, Gregorio Curello |
| 2013 | ITP | Steps towards Verified Implementations of HOL Light. | Magnus O. Myreen, Scott Owens, Ramana Kumar |
| 2013 | PLDI | Translation validation for a verified OS kernel. | Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein |
| 2012 | FMCAD | Decompilation into logic - Improved. | Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind |
| 2012 | ICFP | Proof-producing synthesis of ML from higher-order logic. | Magnus O. Myreen, Scott Owens |
| 2012 | ITP | Functional Programs: Conversions between Deep and Shallow Embeddings. | Magnus O. Myreen |
| 2011 | ITP | A Verified Runtime for a Verified Theorem Prover. | Magnus O. Myreen, Jared Davis |
| 2010 | ITP | A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. | Anthony C. J. Fox, Magnus O. Myreen |
| 2010 | ITP | Separation Logic Adapted for Proofs by Rewriting. | Magnus O. Myreen |
| 2010 | POPL | Verified just-in-time compiler on x86. | Magnus O. Myreen |
| 2009 | CC | Extensible Proof-Producing Compilation. | Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon |
| 2009 | POPL | 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 |
| 2009 | POPL | 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 |
| 2008 | FMCAD | Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. | Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind |
| 2007 | TACAS | Hoare Logic for Realistically Modelled Machine Code. | Magnus O. Myreen, Michael J. C. Gordon |