Tool Support for Invariant Based Programming. - Ralph-Johan Back; Magnus Myreen (APSEC, 2005)

Hoare Logic for ARM Machine Code. - Magnus O. Myreen; Anthony C. J. Fox; Michael J. C. Gordon (FSEN, 2007)

Hoare Logic for Realistically Modelled Machine Code. - Magnus O. Myreen; Michael J. C. Gordon (TACAS, 2007)

Testing and Verifying Invariant Based Programs in the SOCOS Environment. - Ralph-Johan Back; Johannes Eriksson; Magnus Myreen (TAP, 2007)

Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. - Magnus O. Myreen; Michael J. C. Gordon; Konrad Slind (FMCAD, 2008)

Transforming Programs into Recursive Functions. - Magnus O. Myreen; Michael J. C. Gordon (SBMF, 2008)

Extensible Proof-Producing Compilation. - Magnus O. Myreen; Konrad Slind; Michael J. C. Gordon (CC, 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 (DAMP, 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 (POPL, 2009)

Verified LISP Implementations on ARM, x86 and PowerPC. - Magnus O. Myreen; Michael J. C. Gordon (TPHOLs, 2009)

Formal verification of machine-code programs. - Magnus Oskar Myreen (2009)

Specification and Verification of ARM Hardware and Software. - Anthony C. J. Fox; Michael J. C. Gordon; Magnus O. Myreen (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. - Anthony C. J. Fox; Magnus O. Myreen (ITP, 2010)

Separation Logic Adapted for Proofs by Rewriting. - Magnus O. Myreen (ITP, 2010)

Verified just-in-time compiler on x86. - Magnus O. Myreen (POPL, 2010)

Reusable Verification of a Copying Collector. - Magnus O. Myreen (VSTTE, 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)

A Verified Runtime for a Verified Theorem Prover. - Magnus O. Myreen; Jared Davis (ITP, 2011)

Decompilation into logic - Improved. - Magnus O. Myreen; Michael J. C. Gordon; Konrad Slind (FMCAD, 2012)

Proof-producing synthesis of ML from higher-order logic. - Magnus O. Myreen; Scott Owens (ICFP, 2012)

Functional Programs: Conversions between Deep and Shallow Embeddings. - Magnus O. Myreen (ITP, 2012)

Function extraction. - Magnus O. Myreen; Michael J. C. Gordon (Sci. Comput. Program., 2012)

Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. - Magnus O. Myreen; Gregorio Curello (CPP, 2013)

Steps towards Verified Implementations of HOL Light. - Magnus O. Myreen; Scott Owens; Ramana Kumar (ITP, 2013)

Translation validation for a verified OS kernel. - Thomas Arthur Leck Sewell; Magnus O. Myreen; Gerwin Klein (PLDI, 2013)

HOL with Definitions: Semantics, Soundness, and a Verified Implementation. - Ramana Kumar; Rob Arthan; Magnus O. Myreen; Scott Owens (ITP, 2014)

CakeML: a verified implementation of ML. - Ramana Kumar; Magnus O. Myreen; Michael Norrish; Scott Owens (POPL, 2014)

Proof-producing translation of higher-order logic into pure and stateful ML. - Magnus O. Myreen; Scott Owens (J. Funct. Program., 2014)

Pattern Matches in HOL: - A New Representation and Improved Code Generation. - Thomas Tuerk; Magnus O. Myreen; Ramana Kumar (ITP, 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)

Functional Big-Step Semantics. - Scott Owens; Magnus O. Myreen; Ramana Kumar; Yong Kiam Tan (ESOP, 2016)

A new verified compiler backend for CakeML. - Yong Kiam Tan; Magnus O. Myreen; Ramana Kumar; Anthony C. J. Fox; Scott Owens; Michael Norrish (ICFP, 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)

Verified compilation of CakeML to multiple machine-code targets. - Anthony C. J. Fox; Magnus O. Myreen; Yong Kiam Tan; Ramana Kumar (CPP, 2017)

Verified Characteristic Formulae for CakeML. - Armaël Guéneau; Magnus O. Myreen; Ramana Kumar; Michael Norrish (ESOP, 2017)

Automatically Introducing Tail Recursion in CakeML. - Oskar Abrahamsson; Magnus O. Myreen (TFP, 2017)

A Verified Certificate Checker for Floating-Point Error Bounds. - Heiko Becker; Eva Darulova; Magnus O. Myreen (CoRR, 2017)

Verifying efficient function calls in CakeML. - Scott Owens; Michael Norrish; Ramana Kumar; Magnus O. Myreen; Yong Kiam Tan (Proc. ACM Program. Lang., 2017)

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 (IJCAR, 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 (FMCAD, 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 (ITP, 2018)

VeriPhy: verified controller executables from verified cyber-physical system models. - Rose Bohrer; Yong Kiam Tan; Stefan Mitsch; Magnus O. Myreen; André Platzer (PLDI, 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 (VSTTE, 2018)

Clocked Definitions in HOL. - Ramana Kumar; Magnus O. Myreen (CoRR, 2018)

Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler. - Heiko Becker; Eva Darulova; Magnus O. Myreen; Zachary Tatlock (CAV (2), 2019)

A proof-producing translator for verilog development in HOL. - Andreas Lööw; Magnus O. Myreen (FormaliSE@ICSE, 2019)

Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. - Johannes Åman Pohjola; Henrik Rostedt; Magnus O. Myreen (ITP, 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 (PLDI, 2019)

A Verified Generational Garbage Collector for CakeML. - Adam Sandberg Ericsson; Magnus O. Myreen; Johannes Åman Pohjola (J. Autom. Reason., 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)

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)

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)

A minimalistic verified bootstrapped compiler (proof pearl). - Magnus O. Myreen (CPP, 2021)

A flat reachability-based measure for CakeML's cost semantics. - Alejandro Gómez-Londoño; Magnus O. Myreen (IFL, 2021)

The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper). - Magnus O. Myreen (ITP, 2021)

cake_lpr: Verified Propagation Redundancy Checking in CakeML. - Yong Kiam Tan; Marijn J. H. Heule; Magnus O. Myreen (TACAS (2), 2021)

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 (ECOOP, 2022)

Candle: A Verified Implementation of HOL Light. - Oskar Abrahamsson; Magnus O. Myreen; Ramana Kumar; Thomas Sewell (ITP, 2022)

Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. - Hrutvik Kanabar; Anthony C. J. Fox; Magnus O. Myreen (ITP, 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)

Fast, Verified Computation for Candle. - Oskar Abrahamsson; Magnus O. Myreen (ITP, 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 (PLOS@SOSP, 2023)

A Hoare Logic for Diverging Programs. - Johannes Åman Pohjola; Magnus O. Myreen; Miki Tanaka (Arch. Formal Proofs, 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)

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)

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., 2023)

End-to-End Verification for Subgraph Solving. - Stephan Gocht; Ciaran McCreesh; Magnus O. Myreen; Jakob Nordström; Andy Oertel; Yong Kiam Tan (AAAI, 2024)

Formally Certified Approximate Model Counting. - Yong Kiam Tan; Jiong Yang 002; Mate Soos; Magnus O. Myreen; Kuldeep S. Meel (CAV (1), 2024)

Verified Inlining and Specialisation for PureCake. - Hrutvik Kanabar; Kacper Korban; Magnus O. Myreen (ESOP (2), 2024)

Certified MaxSAT Preprocessing. - Hannes Ihalainen; Andy Oertel; Yong Kiam Tan; Jeremias Berg; Matti Järvisalo; Magnus O. Myreen; Jakob Nordström (IJCAR (1), 2024)

Practically Feasible Proof Logging for Pseudo-Boolean Optimization. - Wietze Koops; Daniel Le Berre; Magnus O. Myreen; Jakob Nordström; Andy Oertel; Yong Kiam Tan; Marc Vinyals (CP, 2025)

Efficient Certified Reasoning for Binarized Neural Networks. - Jiong Yang 002; Yong Kiam Tan; Mate Soos; Magnus O. Myreen; Kuldeep S. Meel (SAT, 2025)

Baking for Dafny: A CakeML Backend for Dafny. - Daniel Nezamabadi; Magnus Myreen (CoRR, 2025)

Verifying Device Drivers with Pancake. - Junming Zhao; Alessandro Legnani; Tiana J. Tsang Ung; H. Truong; Tsun Wang Sau; Miki Tanaka; Johannes Åman Pohjola; Thomas Sewell; Robert Sison; Syeda Hira; Magnus Myreen; Michael Norrish; et al. (CoRR, 2025)

Fast, Verified Computation for HOL ITPs. - Oskar Abrahamsson; Magnus O. Myreen; Michael Norrish; Hrutvik Kanabar; Johannes Åman Pohjola (J. Autom. Reason., 2025)

GOL in GOL in HOL: Verified Circuits in Conway's Game of Life. - Magnus O. Myreen; Mario Carneiro (CoRR, 2025)