default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Magnus O. Myreen
@inproceedings{DBLP:conf/aaai/GochtMMNOT24,
author = {Stephan Gocht and
Ciaran McCreesh and
Magnus O. Myreen and
Jakob Nordstr{\"{o}}m and
Andy Oertel and
Yong Kiam Tan},
title = {End-to-End Verification for Subgraph Solving},
booktitle = {{AAAI}},
pages = {8038--8047},
publisher = {{AAAI} Press},
year = {2024}
}
@inproceedings{DBLP:conf/cav/TanYSMM24,
author = {Yong Kiam Tan and
Jiong Yang and
Mate Soos and
Magnus O. Myreen and
Kuldeep S. Meel},
title = {Formally Certified Approximate Model Counting},
booktitle = {{CAV} {(1)}},
series = {Lecture Notes in Computer Science},
volume = {14681},
pages = {153--177},
publisher = {Springer},
year = {2024}
}
@inproceedings{DBLP:conf/esop/KanabarKM24,
author = {Hrutvik Kanabar and
Kacper Korban and
Magnus O. Myreen},
title = {Verified Inlining and Specialisation for PureCake},
booktitle = {{ESOP} {(2)}},
series = {Lecture Notes in Computer Science},
volume = {14577},
pages = {275--301},
publisher = {Springer},
year = {2024}
}
@inproceedings{DBLP:conf/ijcar/IhalainenOTBJMN24,
author = {Hannes Ihalainen and
Andy Oertel and
Yong Kiam Tan and
Jeremias Berg and
Matti J{\"{a}}rvisalo and
Magnus O. Myreen and
Jakob Nordstr{\"{o}}m},
title = {Certified MaxSAT Preprocessing},
booktitle = {{IJCAR} {(1)}},
series = {Lecture Notes in Computer Science},
volume = {14739},
pages = {396--418},
publisher = {Springer},
year = {2024}
}
@article{DBLP:journals/corr/abs-2406-11414,
author = {Yong Kiam Tan and
Jiong Yang and
Mate Soos and
Magnus O. Myreen and
Kuldeep S. Meel},
title = {Formally Certified Approximate Model Counting},
journal = {CoRR},
volume = {abs/2406.11414},
year = {2024}
}
@article{DBLP:journals/afp/PohjolaMT23,
author = {Johannes {\AA}man Pohjola and
Magnus O. Myreen and
Miki Tanaka},
title = {A Hoare Logic for Diverging Programs},
journal = {Arch. Formal Proofs},
volume = {2023},
year = {2023}
}
@article{DBLP:journals/pacmpl/KanabarVAMNPZ23,
author = {Hrutvik Kanabar and
Samuel Vivien and
Oskar Abrahamsson and
Magnus O. Myreen and
Michael Norrish and
Johannes {\AA}man Pohjola and
Riccardo Zanetti},
title = {PureCake: {A} Verified Compiler for a Lazy Functional Language},
journal = {Proc. {ACM} Program. Lang.},
volume = {7},
number = {{PLDI}},
pages = {952--976},
year = {2023}
}
@article{DBLP:journals/pacmpl/SewellMTKMAO23,
author = {Thomas Sewell and
Magnus O. Myreen and
Yong Kiam Tan and
Ramana Kumar and
Alexander Mihajlovic and
Oskar Abrahamsson and
Scott Owens},
title = {Cakes That Bake Cakes: Dynamic Computation in CakeML},
journal = {Proc. {ACM} Program. Lang.},
volume = {7},
number = {{PLDI}},
pages = {1121--1144},
year = {2023}
}
@article{DBLP:journals/sttt/TanHM23,
author = {Yong Kiam Tan and
Marijn J. H. Heule and
Magnus O. Myreen},
title = {Verified Propagation Redundancy and Compositional {UNSAT} Checking
in CakeML},
journal = {Int. J. Softw. Tools Technol. Transf.},
volume = {25},
number = {2},
pages = {167--184},
year = {2023}
}
@inproceedings{DBLP:conf/itp/AbrahamssonM23,
author = {Oskar Abrahamsson and
Magnus O. Myreen},
title = {Fast, Verified Computation for Candle},
booktitle = {{ITP}},
series = {LIPIcs},
volume = {268},
pages = {4:1--4:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2023}
}
@inproceedings{DBLP:conf/plos/PohjolaSTWSNUMS23,
author = {Johannes {\AA}man Pohjola and
Hira Taqdees Syeda and
Miki Tanaka and
Krishnan Winter and
Tsun Wang Sau and
Benjamin Nott and
Tiana J. Tsang Ung and
Craig McLaughlin and
Remy Seassau and
Magnus O. Myreen and
Michael Norrish and
Gernot Heiser},
title = {Pancake: Verified Systems Programming Made Sweeter},
booktitle = {PLOS@SOSP},
pages = {1--9},
publisher = {{ACM}},
year = {2023}
}
@article{DBLP:journals/darts/BeckerRDMTKTF22,
author = {Heiko Becker and
Robert Rabe and
Eva Darulova and
Magnus O. Myreen and
Zachary Tatlock and
Ramana Kumar and
Yong Kiam Tan and
Anthony C. J. Fox},
title = {Verified Compilation and Optimization of Floating-Point Programs in
CakeML (Artifact)},
journal = {Dagstuhl Artifacts Ser.},
volume = {8},
number = {2},
pages = {10:1--10:2},
year = {2022}
}
@inproceedings{DBLP:conf/ecoop/BeckerRDMTKTF22,
author = {Heiko Becker and
Robert Rabe and
Eva Darulova and
Magnus O. Myreen and
Zachary Tatlock and
Ramana Kumar and
Yong Kiam Tan and
Anthony C. J. Fox},
title = {Verified Compilation and Optimization of Floating-Point Programs in
CakeML},
booktitle = {{ECOOP}},
series = {LIPIcs},
volume = {222},
pages = {1:1--1:28},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022}
}
@inproceedings{DBLP:conf/itp/AbrahamssonMKS22,
author = {Oskar Abrahamsson and
Magnus O. Myreen and
Ramana Kumar and
Thomas Sewell},
title = {Candle: {A} Verified Implementation of {HOL} Light},
booktitle = {{ITP}},
series = {LIPIcs},
volume = {237},
pages = {3:1--3:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022}
}
@inproceedings{DBLP:conf/itp/KanabarFM22,
author = {Hrutvik Kanabar and
Anthony C. J. Fox and
Magnus O. Myreen},
title = {Taming an Authoritative Armv8 {ISA} Specification: {L3} Validation
and CakeML Compiler Verification},
booktitle = {{ITP}},
series = {LIPIcs},
volume = {237},
pages = {20:1--20:22},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022}
}
@inproceedings{DBLP:conf/cpp/Myreen21,
author = {Magnus O. Myreen},
title = {A minimalistic verified bootstrapped compiler (proof pearl)},
booktitle = {{CPP}},
pages = {32--45},
publisher = {{ACM}},
year = {2021}
}
@inproceedings{DBLP:conf/ifl/Gomez-LondonoM21,
author = {Alejandro G{\'{o}}mez{-}Londo{\~{n}}o and
Magnus O. Myreen},
title = {A flat reachability-based measure for CakeML's cost semantics},
booktitle = {{IFL}},
pages = {1--9},
publisher = {{ACM}},
year = {2021}
}
@inproceedings{DBLP:conf/itp/Myreen21,
author = {Magnus O. Myreen},
title = {The CakeML Project's Quest for Ever Stronger Correctness Theorems
(Invited Paper)},
booktitle = {{ITP}},
series = {LIPIcs},
volume = {193},
pages = {1:1--1:10},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2021}
}
@inproceedings{DBLP:conf/tacas/TanHM21,
author = {Yong Kiam Tan and
Marijn J. H. Heule and
Magnus O. Myreen},
title = {cake{\_}lpr: Verified Propagation Redundancy Checking in CakeML},
booktitle = {{TACAS} {(2)}},
series = {Lecture Notes in Computer Science},
volume = {12652},
pages = {223--241},
publisher = {Springer},
year = {2021}
}
@article{DBLP:journals/jar/AbrahamssonHKKM20,
author = {Oskar Abrahamsson and
Son Ho and
Hrutvik Kanabar and
Ramana Kumar and
Magnus O. Myreen and
Michael Norrish and
Yong Kiam Tan},
title = {Proof-Producing Synthesis of CakeML from Monadic {HOL} Functions},
journal = {J. Autom. Reason.},
volume = {64},
number = {7},
pages = {1287--1306},
year = {2020}
}
@article{DBLP:journals/pacmpl/Gomez-LondonoPS20,
author = {Alejandro G{\'{o}}mez{-}Londo{\~{n}}o and
Johannes {\AA}man Pohjola and
Hira Taqdees Syeda and
Magnus O. Myreen and
Yong Kiam Tan},
title = {Do you have space for dessert? a verified space cost semantics for
CakeML programs},
journal = {Proc. {ACM} Program. Lang.},
volume = {4},
number = {{OOPSLA}},
pages = {204:1--204:29},
year = {2020}
}
@article{DBLP:journals/jar/EricssonMP19,
author = {Adam Sandberg Ericsson and
Magnus O. Myreen and
Johannes {\AA}man Pohjola},
title = {A Verified Generational Garbage Collector for CakeML},
journal = {J. Autom. Reason.},
volume = {63},
number = {2},
pages = {463--488},
year = {2019}
}
@article{DBLP:journals/jfp/TanMKFON19,
author = {Yong Kiam Tan and
Magnus O. Myreen and
Ramana Kumar and
Anthony C. J. Fox and
Scott Owens and
Michael Norrish},
title = {The verified CakeML compiler backend},
journal = {J. Funct. Program.},
volume = {29},
pages = {e2},
year = {2019}
}
@inproceedings{DBLP:conf/cav/BeckerDMT19,
author = {Heiko Becker and
Eva Darulova and
Magnus O. Myreen and
Zachary Tatlock},
title = {Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler},
booktitle = {{CAV} {(2)}},
series = {Lecture Notes in Computer Science},
volume = {11562},
pages = {155--173},
publisher = {Springer},
year = {2019}
}
@inproceedings{DBLP:conf/icse/LoowM19,
author = {Andreas L{\"{o}}{\"{o}}w and
Magnus O. Myreen},
title = {A proof-producing translator for verilog development in {HOL}},
booktitle = {FormaliSE@ICSE},
pages = {99--108},
publisher = {{IEEE} / {ACM}},
year = {2019}
}
@inproceedings{DBLP:conf/itp/PohjolaRM19,
author = {Johannes {\AA}man Pohjola and
Henrik Rostedt and
Magnus O. Myreen},
title = {Characteristic Formulae for Liveness Properties of Non-Terminating
CakeML Programs},
booktitle = {{ITP}},
series = {LIPIcs},
volume = {141},
pages = {32:1--32:19},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2019}
}
@inproceedings{DBLP:conf/pldi/LoowKTMNAF19,
author = {Andreas L{\"{o}}{\"{o}}w and
Ramana Kumar and
Yong Kiam Tan and
Magnus O. Myreen and
Michael Norrish and
Oskar Abrahamsson and
Anthony C. J. Fox},
title = {Verified compilation on a verified processor},
booktitle = {{PLDI}},
pages = {1041--1053},
publisher = {{ACM}},
year = {2019}
}
@proceedings{DBLP:conf/cpp/2019,
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
publisher = {{ACM}},
year = {2019}
}
@proceedings{DBLP:conf/sfp/2018,
editor = {Michal H. Palka and
Magnus O. Myreen},
title = {Trends in Functional Programming - 19th International Symposium, {TFP}
2018, Gothenburg, Sweden, June 11-13, 2018, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {11457},
publisher = {Springer},
year = {2019}
}
@inproceedings{DBLP:conf/cade/HoAKMTN18,
author = {Son Ho and
Oskar Abrahamsson and
Ramana Kumar and
Magnus O. Myreen and
Yong Kiam Tan and
Michael Norrish},
title = {Proof-Producing Synthesis of CakeML with {I/O} and Local State from
Monadic {HOL} Functions},
booktitle = {{IJCAR}},
series = {Lecture Notes in Computer Science},
volume = {10900},
pages = {646--662},
publisher = {Springer},
year = {2018}
}
@inproceedings{DBLP:conf/fmcad/BeckerZMDMF18,
author = {Heiko Becker and
Nikita Zyuzin and
Rapha{\"{e}}l Monat and
Eva Darulova and
Magnus O. Myreen and
Anthony C. J. Fox},
title = {A Verified Certificate Checker for Finite-Precision Error Bounds in
Coq and {HOL4}},
booktitle = {{FMCAD}},
pages = {1--10},
publisher = {{IEEE}},
year = {2018}
}
@inproceedings{DBLP:conf/itp/KumarMTM18,
author = {Ramana Kumar and
Eric Mullen and
Zachary Tatlock and
Magnus O. Myreen},
title = {Software Verification with ITPs Should Use Binary Code Extraction
to Reduce the {TCB} - (Short Paper)},
booktitle = {{ITP}},
series = {Lecture Notes in Computer Science},
volume = {10895},
pages = {362--369},
publisher = {Springer},
year = {2018}
}
@inproceedings{DBLP:conf/pldi/BohrerTMMP18,
author = {Rose Bohrer and
Yong Kiam Tan and
Stefan Mitsch and
Magnus O. Myreen and
Andr{\'{e}} Platzer},
title = {VeriPhy: verified controller executables from verified cyber-physical
system models},
booktitle = {{PLDI}},
pages = {617--630},
publisher = {{ACM}},
year = {2018}
}
@inproceedings{DBLP:conf/vstte/FereePKOMH18,
author = {Hugo F{\'{e}}r{\'{e}}e and
Johannes {\AA}man Pohjola and
Ramana Kumar and
Scott Owens and
Magnus O. Myreen and
Son Ho},
title = {Program Verification in the Presence of {I/O} - Semantics, Verified
Library Routines, and Verified Applications},
booktitle = {{VSTTE}},
series = {Lecture Notes in Computer Science},
volume = {11294},
pages = {88--111},
publisher = {Springer},
year = {2018}
}
@article{DBLP:journals/corr/abs-1803-03417,
author = {Ramana Kumar and
Magnus O. Myreen},
title = {Clocked Definitions in {HOL}},
journal = {CoRR},
volume = {abs/1803.03417},
year = {2018}
}
@article{DBLP:journals/pacmpl/OwensNKMT17,
author = {Scott Owens and
Michael Norrish and
Ramana Kumar and
Magnus O. Myreen and
Yong Kiam Tan},
title = {Verifying efficient function calls in CakeML},
journal = {Proc. {ACM} Program. Lang.},
volume = {1},
number = {{ICFP}},
pages = {18:1--18:27},
year = {2017}
}
@inproceedings{DBLP:conf/cpp/FoxMTK17,
author = {Anthony C. J. Fox and
Magnus O. Myreen and
Yong Kiam Tan and
Ramana Kumar},
title = {Verified compilation of CakeML to multiple machine-code targets},
booktitle = {{CPP}},
pages = {125--137},
publisher = {{ACM}},
year = {2017}
}
@inproceedings{DBLP:conf/esop/GueneauMKN17,
author = {Arma{\"{e}}l Gu{\'{e}}neau and
Magnus O. Myreen and
Ramana Kumar and
Michael Norrish},
title = {Verified Characteristic Formulae for CakeML},
booktitle = {{ESOP}},
series = {Lecture Notes in Computer Science},
volume = {10201},
pages = {584--610},
publisher = {Springer},
year = {2017}
}
@inproceedings{DBLP:conf/itp/EricssonMP17,
author = {Adam Sandberg Ericsson and
Magnus O. Myreen and
Johannes {\AA}man Pohjola},
title = {A Verified Generational Garbage Collector for CakeML},
booktitle = {{ITP}},
series = {Lecture Notes in Computer Science},
volume = {10499},
pages = {444--461},
publisher = {Springer},
year = {2017}
}
@inproceedings{DBLP:conf/sfp/AbrahamssonM17,
author = {Oskar Abrahamsson and
Magnus O. Myreen},
title = {Automatically Introducing Tail Recursion in CakeML},
booktitle = {{TFP}},
series = {Lecture Notes in Computer Science},
volume = {10788},
pages = {118--134},
publisher = {Springer},
year = {2017}
}
@article{DBLP:journals/corr/BeckerDM17,
author = {Heiko Becker and
Eva Darulova and
Magnus O. Myreen},
title = {A Verified Certificate Checker for Floating-Point Error Bounds},
journal = {CoRR},
volume = {abs/1707.02115},
year = {2017}
}
@article{DBLP:journals/jar/KumarAMO16,
author = {Ramana Kumar and
Rob Arthan and
Magnus O. Myreen and
Scott Owens},
title = {Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and
a Verified Implementation},
journal = {J. Autom. Reason.},
volume = {56},
number = {3},
pages = {221--259},
year = {2016}
}
@inproceedings{DBLP:conf/esop/OwensMKT16,
author = {Scott Owens and
Magnus O. Myreen and
Ramana Kumar and
Yong Kiam Tan},
title = {Functional Big-Step Semantics},
booktitle = {{ESOP}},
series = {Lecture Notes in Computer Science},
volume = {9632},
pages = {589--615},
publisher = {Springer},
year = {2016}
}
@inproceedings{DBLP:conf/icfp/TanMKFON16,
author = {Yong Kiam Tan and
Magnus O. Myreen and
Ramana Kumar and
Anthony C. J. Fox and
Scott Owens and
Michael Norrish},
title = {A new verified compiler backend for CakeML},
booktitle = {{ICFP}},
pages = {60--73},
publisher = {{ACM}},
year = {2016}
}
@article{DBLP:journals/jar/DavisM15,
author = {Jared Davis and
Magnus O. Myreen},
title = {The Reflective Milawa Theorem Prover is Sound (Down to the Machine
Code that Runs it)},
journal = {J. Autom. Reason.},
volume = {55},
number = {2},
pages = {117--183},
year = {2015}
}
@inproceedings{DBLP:conf/itp/TuerkMK15,
author = {Thomas Tuerk and
Magnus O. Myreen and
Ramana Kumar},
title = {Pattern Matches in {HOL:} - {A} New Representation and Improved Code
Generation},
booktitle = {{ITP}},
series = {Lecture Notes in Computer Science},
volume = {9236},
pages = {453--468},
publisher = {Springer},
year = {2015}
}
@article{DBLP:journals/jfp/MyreenO14,
author = {Magnus O. Myreen and
Scott Owens},
title = {Proof-producing translation of higher-order logic into pure and stateful
{ML}},
journal = {J. Funct. Program.},
volume = {24},
number = {2-3},
pages = {284--315},
year = {2014}
}
@inproceedings{DBLP:conf/itp/KumarAMO14,
author = {Ramana Kumar and
Rob Arthan and
Magnus O. Myreen and
Scott Owens},
title = {{HOL} with Definitions: Semantics, Soundness, and a Verified Implementation},
booktitle = {{ITP}},
series = {Lecture Notes in Computer Science},
volume = {8558},
pages = {308--324},
publisher = {Springer},
year = {2014}
}
@inproceedings{DBLP:conf/itp/MyreenD14,
author = {Magnus O. Myreen and
Jared Davis},
title = {The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine
Code That Runs It)},
booktitle = {{ITP}},
series = {Lecture Notes in Computer Science},
volume = {8558},
pages = {421--436},
publisher = {Springer},
year = {2014}
}
@inproceedings{DBLP:conf/popl/KumarMNO14,
author = {Ramana Kumar and
Magnus O. Myreen and
Michael Norrish and
Scott Owens},
title = {CakeML: a verified implementation of {ML}},
booktitle = {{POPL}},
pages = {179--192},
publisher = {{ACM}},
year = {2014}
}
@inproceedings{DBLP:conf/cpp/MyreenC13,
author = {Magnus O. Myreen and
Gregorio Curello},
title = {Proof Pearl: {A} Verified Bignum Implementation in x86-64 Machine
Code},
booktitle = {{CPP}},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {66--81},
publisher = {Springer},
year = {2013}
}
@inproceedings{DBLP:conf/itp/MyreenOK13,
author = {Magnus O. Myreen and
Scott Owens and
Ramana Kumar},
title = {Steps towards Verified Implementations of {HOL} Light},
booktitle = {{ITP}},
series = {Lecture Notes in Computer Science},
volume = {7998},
pages = {490--495},
publisher = {Springer},
year = {2013}
}
@inproceedings{DBLP:conf/pldi/SewellMK13,
author = {Thomas Arthur Leck Sewell and
Magnus O. Myreen and
Gerwin Klein},
title = {Translation validation for a verified {OS} kernel},
booktitle = {{PLDI}},
pages = {471--482},
publisher = {{ACM}},
year = {2013}
}
@article{DBLP:journals/scp/MyreenG12,
author = {Magnus O. Myreen and
Michael J. C. Gordon},
title = {Function extraction},
journal = {Sci. Comput. Program.},
volume = {77},
number = {4},
pages = {505--517},
year = {2012}
}
@inproceedings{DBLP:conf/fmcad/MyreenGS12,
author = {Magnus O. Myreen and
Michael J. C. Gordon and
Konrad Slind},
title = {Decompilation into logic - Improved},
booktitle = {{FMCAD}},
pages = {78--81},
publisher = {{IEEE}},
year = {2012}
}
@inproceedings{DBLP:conf/icfp/MyreenO12,
author = {Magnus O. Myreen and
Scott Owens},
title = {Proof-producing synthesis of {ML} from higher-order logic},
booktitle = {{ICFP}},
pages = {115--126},
publisher = {{ACM}},
year = {2012}
}
@inproceedings{DBLP:conf/itp/Myreen12,
author = {Magnus O. Myreen},
title = {Functional Programs: Conversions between Deep and Shallow Embeddings},
booktitle = {{ITP}},
series = {Lecture Notes in Computer Science},
volume = {7406},
pages = {412--417},
publisher = {Springer},
year = {2012}
}
@inproceedings{DBLP:conf/itp/MyreenD11,
author = {Magnus O. Myreen and
Jared Davis},
title = {A Verified Runtime for a Verified Theorem Prover},
booktitle = {{ITP}},
series = {Lecture Notes in Computer Science},
volume = {6898},
pages = {265--280},
publisher = {Springer},
year = {2011}
}
@article{DBLP:journals/cacm/SewellSONM10,
author = {Peter Sewell and
Susmit Sarkar and
Scott Owens and
Francesco Zappa Nardelli and
Magnus O. Myreen},
title = {x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors},
journal = {Commun. {ACM}},
volume = {53},
number = {7},
pages = {89--97},
year = {2010}
}
@inproceedings{DBLP:conf/itp/FoxM10,
author = {Anthony C. J. Fox and
Magnus O. Myreen},
title = {A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture},
booktitle = {{ITP}},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {243--258},
publisher = {Springer},
year = {2010}
}
@inproceedings{DBLP:conf/itp/Myreen10,
author = {Magnus O. Myreen},
title = {Separation Logic Adapted for Proofs by Rewriting},
booktitle = {{ITP}},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {485--489},
publisher = {Springer},
year = {2010}
}
@inproceedings{DBLP:conf/popl/Myreen10,
author = {Magnus O. Myreen},
title = {Verified just-in-time compiler on x86},
booktitle = {{POPL}},
pages = {107--118},
publisher = {{ACM}},
year = {2010}
}
@inproceedings{DBLP:conf/vstte/Myreen10,
author = {Magnus O. Myreen},
title = {Reusable Verification of a Copying Collector},
booktitle = {{VSTTE}},
series = {Lecture Notes in Computer Science},
volume = {6217},
pages = {142--156},
publisher = {Springer},
year = {2010}
}
@incollection{DBLP:books/sp/10/FoxGM10,
author = {Anthony C. J. Fox and
Michael J. C. Gordon and
Magnus O. Myreen},
title = {Specification and Verification of {ARM} Hardware and Software},
booktitle = {Design and Verification of Microprocessor Systems for High-Assurance
Applications},
pages = {221--247},
publisher = {Springer},
year = {2010}
}
@phdthesis{DBLP:phd/ethos/Myreen09,
author = {Magnus Oskar Myreen},
title = {Formal verification of machine-code programs},
school = {University of Cambridge, {UK}},
year = {2009}
}
@inproceedings{DBLP:conf/cc/MyreenSG09,
author = {Magnus O. Myreen and
Konrad Slind and
Michael J. C. Gordon},
title = {Extensible Proof-Producing Compilation},
booktitle = {{CC}},
series = {Lecture Notes in Computer Science},
volume = {5501},
pages = {2--16},
publisher = {Springer},
year = {2009}
}
@inproceedings{DBLP:conf/popl/AlglaveFIMSSN09,
author = {Jade Alglave and
Anthony C. J. Fox and
Samin Ishtiaq and
Magnus O. Myreen and
Susmit Sarkar and
Peter Sewell and
Francesco Zappa Nardelli},
title = {The semantics of power and {ARM} multiprocessor machine code},
booktitle = {{DAMP}},
pages = {13--24},
publisher = {{ACM}},
year = {2009}
}
@inproceedings{DBLP:conf/popl/SarkarSNORBMA09,
author = {Susmit Sarkar and
Peter Sewell and
Francesco Zappa Nardelli and
Scott Owens and
Tom Ridge and
Thomas Braibant and
Magnus O. Myreen and
Jade Alglave},
title = {The semantics of x86-CC multiprocessor machine code},
booktitle = {{POPL}},
pages = {379--391},
publisher = {{ACM}},
year = {2009}
}
@inproceedings{DBLP:conf/tphol/MyreenG09,
author = {Magnus O. Myreen and
Michael J. C. Gordon},
title = {Verified {LISP} Implementations on ARM, x86 and PowerPC},
booktitle = {TPHOLs},
series = {Lecture Notes in Computer Science},
volume = {5674},
pages = {359--374},
publisher = {Springer},
year = {2009}
}
@inproceedings{DBLP:conf/fmcad/MyreenGS08,
author = {Magnus O. Myreen and
Michael J. C. Gordon and
Konrad Slind},
title = {Machine-Code Verification for Multiple Architectures - An Application
of Decompilation into Logic},
booktitle = {{FMCAD}},
pages = {1--8},
publisher = {{IEEE}},
year = {2008}
}
@inproceedings{DBLP:journals/entcs/MyreenG09,
author = {Magnus O. Myreen and
Michael J. C. Gordon},
title = {Transforming Programs into Recursive Functions},
booktitle = {{SBMF}},
series = {Electronic Notes in Theoretical Computer Science},
volume = {240},
pages = {185--200},
publisher = {Elsevier},
year = {2008}
}
@inproceedings{DBLP:conf/fsen/MyreenFG07,
author = {Magnus O. Myreen and
Anthony C. J. Fox and
Michael J. C. Gordon},
title = {Hoare Logic for {ARM} Machine Code},
booktitle = {{FSEN}},
series = {Lecture Notes in Computer Science},
volume = {4767},
pages = {272--286},
publisher = {Springer},
year = {2007}
}
@inproceedings{DBLP:conf/tacas/MyreenG07,
author = {Magnus O. Myreen and
Michael J. C. Gordon},
title = {Hoare Logic for Realistically Modelled Machine Code},
booktitle = {{TACAS}},
series = {Lecture Notes in Computer Science},
volume = {4424},
pages = {568--582},
publisher = {Springer},
year = {2007}
}
@inproceedings{DBLP:conf/tap/BackEM07,
author = {Ralph{-}Johan Back and
Johannes Eriksson and
Magnus Myreen},
title = {Testing and Verifying Invariant Based Programs in the {SOCOS} Environment},
booktitle = {{TAP}},
series = {Lecture Notes in Computer Science},
volume = {4454},
pages = {61--78},
publisher = {Springer},
year = {2007}
}
@inproceedings{DBLP:conf/apsec/BackM05,
author = {Ralph{-}Johan Back and
Magnus Myreen},
title = {Tool Support for Invariant Based Programming},
booktitle = {{APSEC}},
pages = {711--718},
publisher = {{IEEE} Computer Society},
year = {2005}
}
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-08-23 19:24 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
