Stop the war!Остановите войну!
for scientists:
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},
editor = {Michael J. Wooldridge and
Jennifer G. Dy and
Sriraam Natarajan},
title = {End-to-End Verification for Subgraph Solving},
booktitle = {Thirty-Eighth {AAAI} Conference on Artificial Intelligence, {AAAI}
2024, Thirty-Sixth Conference on Innovative Applications of Artificial
Intelligence, {IAAI} 2024, Fourteenth Symposium on Educational Advances
in Artificial Intelligence, {EAAI} 2014, February 20-27, 2024, Vancouver,
Canada},
pages = {8038--8047},
publisher = {{AAAI} Press},
year = {2024},
url = {https://doi.org/10.1609/aaai.v38i8.28642},
doi = {10.1609/AAAI.V38I8.28642},
timestamp = {Tue, 02 Apr 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/aaai/GochtMMNOT24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/KanabarKM24,
author = {Hrutvik Kanabar and
Kacper Korban and
Magnus O. Myreen},
editor = {Stephanie Weirich},
title = {Verified Inlining and Specialisation for PureCake},
booktitle = {Programming Languages and Systems - 33rd European Symposium on Programming,
{ESOP} 2024, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2024, Luxembourg City, Luxembourg,
April 6-11, 2024, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {14577},
pages = {275--301},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-57267-8\_11},
doi = {10.1007/978-3-031-57267-8\_11},
timestamp = {Sun, 14 Apr 2024 18:32:18 +0200},
biburl = {https://dblp.org/rec/conf/esop/KanabarKM24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://www.isa-afp.org/entries/HoareForDivergence.html},
timestamp = {Tue, 18 Apr 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/PohjolaMT23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1145/3591259},
doi = {10.1145/3591259},
timestamp = {Sun, 22 Oct 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/pacmpl/KanabarVAMNPZ23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1145/3591266},
doi = {10.1145/3591266},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/pacmpl/SewellMTKMAO23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1007/s10009-022-00690-y},
doi = {10.1007/S10009-022-00690-Y},
timestamp = {Sat, 13 May 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sttt/TanHM23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/AbrahamssonM23,
author = {Oskar Abrahamsson and
Magnus O. Myreen},
editor = {Adam Naumowicz and
Ren{\'{e}} Thiemann},
title = {Fast, Verified Computation for Candle},
booktitle = {14th International Conference on Interactive Theorem Proving, {ITP}
2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
series = {LIPIcs},
volume = {268},
pages = {4:1--4:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2023},
url = {https://doi.org/10.4230/LIPIcs.ITP.2023.4},
doi = {10.4230/LIPICS.ITP.2023.4},
timestamp = {Wed, 26 Jul 2023 16:07:09 +0200},
biburl = {https://dblp.org/rec/conf/itp/AbrahamssonM23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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 = {Proceedings of the 12th Workshop on Programming Languages and Operating
Systems, {PLOS} 2023, Koblenz, Germany, 23 October 2023},
pages = {1--9},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3623759.3624544},
doi = {10.1145/3623759.3624544},
timestamp = {Fri, 27 Oct 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/plos/PohjolaSTWSNUMS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.4230/DARTS.8.2.10},
doi = {10.4230/DARTS.8.2.10},
timestamp = {Thu, 23 Jun 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/darts/BeckerRDMTKTF22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
editor = {Karim Ali and
Jan Vitek},
title = {Verified Compilation and Optimization of Floating-Point Programs in
CakeML},
booktitle = {36th European Conference on Object-Oriented Programming, {ECOOP} 2022,
June 6-10, 2022, Berlin, Germany},
series = {LIPIcs},
volume = {222},
pages = {1:1--1:28},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022},
url = {https://doi.org/10.4230/LIPIcs.ECOOP.2022.1},
doi = {10.4230/LIPICS.ECOOP.2022.1},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ecoop/BeckerRDMTKTF22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/AbrahamssonMKS22,
author = {Oskar Abrahamsson and
Magnus O. Myreen and
Ramana Kumar and
Thomas Sewell},
editor = {June Andronick and
Leonardo de Moura},
title = {Candle: {A} Verified Implementation of {HOL} Light},
booktitle = {13th International Conference on Interactive Theorem Proving, {ITP}
2022, August 7-10, 2022, Haifa, Israel},
series = {LIPIcs},
volume = {237},
pages = {3:1--3:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022},
url = {https://doi.org/10.4230/LIPIcs.ITP.2022.3},
doi = {10.4230/LIPICS.ITP.2022.3},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/AbrahamssonMKS22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/KanabarFM22,
author = {Hrutvik Kanabar and
Anthony C. J. Fox and
Magnus O. Myreen},
editor = {June Andronick and
Leonardo de Moura},
title = {Taming an Authoritative Armv8 {ISA} Specification: {L3} Validation
and CakeML Compiler Verification},
booktitle = {13th International Conference on Interactive Theorem Proving, {ITP}
2022, August 7-10, 2022, Haifa, Israel},
series = {LIPIcs},
volume = {237},
pages = {20:1--20:22},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022},
url = {https://doi.org/10.4230/LIPIcs.ITP.2022.20},
doi = {10.4230/LIPICS.ITP.2022.20},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/KanabarFM22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Myreen21,
author = {Magnus O. Myreen},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {A minimalistic verified bootstrapped compiler (proof pearl)},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {32--45},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439915},
doi = {10.1145/3437992.3439915},
timestamp = {Fri, 12 Feb 2021 14:28:33 +0100},
biburl = {https://dblp.org/rec/conf/cpp/Myreen21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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 = {33rd Symposium on Implementation and Application of Functional Languages,
{IFL} 2021, Nijmegen, The Netherlands, September 1-3, 2021},
pages = {1--9},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3544885.3544887},
doi = {10.1145/3544885.3544887},
timestamp = {Mon, 14 Nov 2022 12:07:39 +0100},
biburl = {https://dblp.org/rec/conf/ifl/Gomez-LondonoM21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/Myreen21,
author = {Magnus O. Myreen},
editor = {Liron Cohen and
Cezary Kaliszyk},
title = {The CakeML Project's Quest for Ever Stronger Correctness Theorems
(Invited Paper)},
booktitle = {12th International Conference on Interactive Theorem Proving, {ITP}
2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
series = {LIPIcs},
volume = {193},
pages = {1:1--1:10},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2021},
url = {https://doi.org/10.4230/LIPIcs.ITP.2021.1},
doi = {10.4230/LIPICS.ITP.2021.1},
timestamp = {Mon, 21 Jun 2021 14:45:49 +0200},
biburl = {https://dblp.org/rec/conf/itp/Myreen21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/TanHM21,
author = {Yong Kiam Tan and
Marijn J. H. Heule and
Magnus O. Myreen},
editor = {Jan Friso Groote and
Kim Guldstrand Larsen},
title = {cake{\_}lpr: Verified Propagation Redundancy Checking in CakeML},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 27th International Conference, {TACAS} 2021, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings,
Part {II}},
series = {Lecture Notes in Computer Science},
volume = {12652},
pages = {223--241},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-72013-1\_12},
doi = {10.1007/978-3-030-72013-1\_12},
timestamp = {Fri, 14 May 2021 08:34:19 +0200},
biburl = {https://dblp.org/rec/conf/tacas/TanHM21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1007/s10817-020-09559-8},
doi = {10.1007/S10817-020-09559-8},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/AbrahamssonHKKM20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1145/3428272},
doi = {10.1145/3428272},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/pacmpl/Gomez-LondonoPS20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1007/s10817-018-9487-z},
doi = {10.1007/S10817-018-9487-Z},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/EricssonMP19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1017/S0956796818000229},
doi = {10.1017/S0956796818000229},
timestamp = {Sun, 22 Oct 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfp/TanMKFON19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/BeckerDMT19,
author = {Heiko Becker and
Eva Darulova and
Magnus O. Myreen and
Zachary Tatlock},
editor = {Isil Dillig and
Serdar Tasiran},
title = {Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler},
booktitle = {Computer Aided Verification - 31st International Conference, {CAV}
2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part
{II}},
series = {Lecture Notes in Computer Science},
volume = {11562},
pages = {155--173},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-25543-5\_10},
doi = {10.1007/978-3-030-25543-5\_10},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cav/BeckerDMT19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icse/LoowM19,
author = {Andreas L{\"{o}}{\"{o}}w and
Magnus O. Myreen},
editor = {Stefania Gnesi and
Nico Plat and
Nancy A. Day and
Matteo Rossi},
title = {A proof-producing translator for verilog development in {HOL}},
booktitle = {Proceedings of the 7th International Workshop on Formal Methods in
Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May
27, 2019},
pages = {99--108},
publisher = {{IEEE} / {ACM}},
year = {2019},
url = {https://doi.org/10.1109/FormaliSE.2019.00020},
doi = {10.1109/FORMALISE.2019.00020},
timestamp = {Wed, 16 Oct 2019 14:14:49 +0200},
biburl = {https://dblp.org/rec/conf/icse/LoowM19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/PohjolaRM19,
author = {Johannes {\AA}man Pohjola and
Henrik Rostedt and
Magnus O. Myreen},
editor = {John Harrison and
John O'Leary and
Andrew Tolmach},
title = {Characteristic Formulae for Liveness Properties of Non-Terminating
CakeML Programs},
booktitle = {10th International Conference on Interactive Theorem Proving, {ITP}
2019, September 9-12, 2019, Portland, OR, {USA}},
series = {LIPIcs},
volume = {141},
pages = {32:1--32:19},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2019},
url = {https://doi.org/10.4230/LIPIcs.ITP.2019.32},
doi = {10.4230/LIPICS.ITP.2019.32},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/PohjolaRM19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
editor = {Kathryn S. McKinley and
Kathleen Fisher},
title = {Verified compilation on a verified processor},
booktitle = {Proceedings of the 40th {ACM} {SIGPLAN} Conference on Programming
Language Design and Implementation, {PLDI} 2019, Phoenix, AZ, USA,
June 22-26, 2019},
pages = {1041--1053},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3314221.3314622},
doi = {10.1145/3314221.3314622},
timestamp = {Mon, 26 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/pldi/LoowKTMNAF19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://dl.acm.org/citation.cfm?id=3293880},
isbn = {978-1-4503-6222-1},
timestamp = {Fri, 04 Jan 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/2019.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1007/978-3-030-18506-0},
doi = {10.1007/978-3-030-18506-0},
isbn = {978-3-030-18505-3},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/sfp/2018.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
editor = {Didier Galmiche and
Stephan Schulz and
Roberto Sebastiani},
title = {Proof-Producing Synthesis of CakeML with {I/O} and Local State from
Monadic {HOL} Functions},
booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 14-17, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10900},
pages = {646--662},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94205-6\_42},
doi = {10.1007/978-3-319-94205-6\_42},
timestamp = {Mon, 28 Aug 2023 21:17:45 +0200},
biburl = {https://dblp.org/rec/conf/cade/HoAKMTN18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
editor = {Nikolaj S. Bj{\o}rner and
Arie Gurfinkel},
title = {A Verified Certificate Checker for Finite-Precision Error Bounds in
Coq and {HOL4}},
booktitle = {2018 Formal Methods in Computer Aided Design, {FMCAD} 2018, Austin,
TX, USA, October 30 - November 2, 2018},
pages = {1--10},
publisher = {{IEEE}},
year = {2018},
url = {https://doi.org/10.23919/FMCAD.2018.8603019},
doi = {10.23919/FMCAD.2018.8603019},
timestamp = {Thu, 14 Apr 2022 20:26:15 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/BeckerZMDMF18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/KumarMTM18,
author = {Ramana Kumar and
Eric Mullen and
Zachary Tatlock and
Magnus O. Myreen},
editor = {Jeremy Avigad and
Assia Mahboubi},
title = {Software Verification with ITPs Should Use Binary Code Extraction
to Reduce the {TCB} - (Short Paper)},
booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 9-12, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10895},
pages = {362--369},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94821-8\_21},
doi = {10.1007/978-3-319-94821-8\_21},
timestamp = {Sun, 12 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/itp/KumarMTM18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/BohrerTMMP18,
author = {Rose Bohrer and
Yong Kiam Tan and
Stefan Mitsch and
Magnus O. Myreen and
Andr{\'{e}} Platzer},
editor = {Jeffrey S. Foster and
Dan Grossman},
title = {VeriPhy: verified controller executables from verified cyber-physical
system models},
booktitle = {Proceedings of the 39th {ACM} {SIGPLAN} Conference on Programming
Language Design and Implementation, {PLDI} 2018, Philadelphia, PA,
USA, June 18-22, 2018},
pages = {617--630},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3192366.3192406},
doi = {10.1145/3192366.3192406},
timestamp = {Tue, 10 May 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/pldi/BohrerTMMP18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
editor = {Ruzica Piskac and
Philipp R{\"{u}}mmer},
title = {Program Verification in the Presence of {I/O} - Semantics, Verified
Library Routines, and Verified Applications},
booktitle = {Verified Software. Theories, Tools, and Experiments - 10th International
Conference, {VSTTE} 2018, Oxford, UK, July 18-19, 2018, Revised Selected
Papers},
series = {Lecture Notes in Computer Science},
volume = {11294},
pages = {88--111},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-030-03592-1\_6},
doi = {10.1007/978-3-030-03592-1\_6},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/vstte/FereePKOMH18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {http://arxiv.org/abs/1803.03417},
eprinttype = {arXiv},
eprint = {1803.03417},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1803-03417.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1145/3110262},
doi = {10.1145/3110262},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/OwensNKMT17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FoxMTK17,
author = {Anthony C. J. Fox and
Magnus O. Myreen and
Yong Kiam Tan and
Ramana Kumar},
editor = {Yves Bertot and
Viktor Vafeiadis},
title = {Verified compilation of CakeML to multiple machine-code targets},
booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
pages = {125--137},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3018610.3018621},
doi = {10.1145/3018610.3018621},
timestamp = {Tue, 06 Nov 2018 16:59:23 +0100},
biburl = {https://dblp.org/rec/conf/cpp/FoxMTK17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/GueneauMKN17,
author = {Arma{\"{e}}l Gu{\'{e}}neau and
Magnus O. Myreen and
Ramana Kumar and
Michael Norrish},
editor = {Hongseok Yang},
title = {Verified Characteristic Formulae for CakeML},
booktitle = {Programming Languages and Systems - 26th European Symposium on Programming,
{ESOP} 2017, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29,
2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10201},
pages = {584--610},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-662-54434-1\_22},
doi = {10.1007/978-3-662-54434-1\_22},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/esop/GueneauMKN17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/EricssonMP17,
author = {Adam Sandberg Ericsson and
Magnus O. Myreen and
Johannes {\AA}man Pohjola},
editor = {Mauricio Ayala{-}Rinc{\'{o}}n and
C{\'{e}}sar A. Mu{\~{n}}oz},
title = {A Verified Generational Garbage Collector for CakeML},
booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP}
2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10499},
pages = {444--461},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-66107-0\_28},
doi = {10.1007/978-3-319-66107-0\_28},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/EricssonMP17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sfp/AbrahamssonM17,
author = {Oskar Abrahamsson and
Magnus O. Myreen},
editor = {Meng Wang and
Scott Owens},
title = {Automatically Introducing Tail Recursion in CakeML},
booktitle = {Trends in Functional Programming - 18th International Symposium, {TFP}
2017, Canterbury, UK, June 19-21, 2017, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {10788},
pages = {118--134},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-89719-6\_7},
doi = {10.1007/978-3-319-89719-6\_7},
timestamp = {Wed, 07 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/sfp/AbrahamssonM17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {http://arxiv.org/abs/1707.02115},
eprinttype = {arXiv},
eprint = {1707.02115},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BeckerDM17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1007/s10817-015-9357-x},
doi = {10.1007/S10817-015-9357-X},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/KumarAMO16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/OwensMKT16,
author = {Scott Owens and
Magnus O. Myreen and
Ramana Kumar and
Yong Kiam Tan},
editor = {Peter Thiemann},
title = {Functional Big-Step Semantics},
booktitle = {Programming Languages and Systems - 25th European Symposium on Programming,
{ESOP} 2016, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands,
April 2-8, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9632},
pages = {589--615},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-662-49498-1\_23},
doi = {10.1007/978-3-662-49498-1\_23},
timestamp = {Mon, 23 Mar 2020 12:22:51 +0100},
biburl = {https://dblp.org/rec/conf/esop/OwensMKT16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
editor = {Jacques Garrigue and
Gabriele Keller and
Eijiro Sumii},
title = {A new verified compiler backend for CakeML},
booktitle = {Proceedings of the 21st {ACM} {SIGPLAN} International Conference on
Functional Programming, {ICFP} 2016, Nara, Japan, September 18-22,
2016},
pages = {60--73},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2951913.2951924},
doi = {10.1145/2951913.2951924},
timestamp = {Sat, 21 Oct 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/icfp/TanMKFON16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1007/s10817-015-9324-6},
doi = {10.1007/S10817-015-9324-6},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/DavisM15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/TuerkMK15,
author = {Thomas Tuerk and
Magnus O. Myreen and
Ramana Kumar},
editor = {Christian Urban and
Xingyuan Zhang},
title = {Pattern Matches in {HOL:} - {A} New Representation and Improved Code
Generation},
booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP}
2015, Nanjing, China, August 24-27, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9236},
pages = {453--468},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-22102-1\_30},
doi = {10.1007/978-3-319-22102-1\_30},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/TuerkMK15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1017/S0956796813000282},
doi = {10.1017/S0956796813000282},
timestamp = {Tue, 06 Jun 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfp/MyreenO14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/KumarAMO14,
author = {Ramana Kumar and
Rob Arthan and
Magnus O. Myreen and
Scott Owens},
editor = {Gerwin Klein and
Ruben Gamboa},
title = {{HOL} with Definitions: Semantics, Soundness, and a Verified Implementation},
booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 14-17, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8558},
pages = {308--324},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08970-6\_20},
doi = {10.1007/978-3-319-08970-6\_20},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/KumarAMO14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/MyreenD14,
author = {Magnus O. Myreen and
Jared Davis},
editor = {Gerwin Klein and
Ruben Gamboa},
title = {The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine
Code That Runs It)},
booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 14-17, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8558},
pages = {421--436},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08970-6\_27},
doi = {10.1007/978-3-319-08970-6\_27},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/MyreenD14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/KumarMNO14,
author = {Ramana Kumar and
Magnus O. Myreen and
Michael Norrish and
Scott Owens},
editor = {Suresh Jagannathan and
Peter Sewell},
title = {CakeML: a verified implementation of {ML}},
booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21,
2014},
pages = {179--192},
publisher = {{ACM}},
year = {2014},
url = {https://doi.org/10.1145/2535838.2535841},
doi = {10.1145/2535838.2535841},
timestamp = {Thu, 24 Jun 2021 16:19:31 +0200},
biburl = {https://dblp.org/rec/conf/popl/KumarMNO14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/MyreenC13,
author = {Magnus O. Myreen and
Gregorio Curello},
editor = {Georges Gonthier and
Michael Norrish},
title = {Proof Pearl: {A} Verified Bignum Implementation in x86-64 Machine
Code},
booktitle = {Certified Programs and Proofs - Third International Conference, {CPP}
2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8307},
pages = {66--81},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-319-03545-1\_5},
doi = {10.1007/978-3-319-03545-1\_5},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/cpp/MyreenC13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/MyreenOK13,
author = {Magnus O. Myreen and
Scott Owens and
Ramana Kumar},
editor = {Sandrine Blazy and
Christine Paulin{-}Mohring and
David Pichardie},
title = {Steps towards Verified Implementations of {HOL} Light},
booktitle = {Interactive Theorem Proving - 4th International Conference, {ITP}
2013, Rennes, France, July 22-26, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7998},
pages = {490--495},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39634-2\_38},
doi = {10.1007/978-3-642-39634-2\_38},
timestamp = {Wed, 25 Sep 2019 18:17:56 +0200},
biburl = {https://dblp.org/rec/conf/itp/MyreenOK13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pldi/SewellMK13,
author = {Thomas Arthur Leck Sewell and
Magnus O. Myreen and
Gerwin Klein},
editor = {Hans{-}Juergen Boehm and
Cormac Flanagan},
title = {Translation validation for a verified {OS} kernel},
booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
{PLDI} '13, Seattle, WA, USA, June 16-19, 2013},
pages = {471--482},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2491956.2462183},
doi = {10.1145/2491956.2462183},
timestamp = {Fri, 30 Nov 2018 12:21:40 +0100},
biburl = {https://dblp.org/rec/conf/pldi/SewellMK13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1016/j.scico.2010.10.001},
doi = {10.1016/J.SCICO.2010.10.001},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/scp/MyreenG12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/MyreenGS12,
author = {Magnus O. Myreen and
Michael J. C. Gordon and
Konrad Slind},
editor = {Gianpiero Cabodi and
Satnam Singh},
title = {Decompilation into logic - Improved},
booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2012, Cambridge,
UK, October 22-25, 2012},
pages = {78--81},
publisher = {{IEEE}},
year = {2012},
url = {https://ieeexplore.ieee.org/document/6462558/},
timestamp = {Mon, 09 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/MyreenGS12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/MyreenO12,
author = {Magnus O. Myreen and
Scott Owens},
editor = {Peter Thiemann and
Robby Bruce Findler},
title = {Proof-producing synthesis of {ML} from higher-order logic},
booktitle = {{ACM} {SIGPLAN} International Conference on Functional Programming,
ICFP'12, Copenhagen, Denmark, September 9-15, 2012},
pages = {115--126},
publisher = {{ACM}},
year = {2012},
url = {https://doi.org/10.1145/2364527.2364545},
doi = {10.1145/2364527.2364545},
timestamp = {Thu, 24 Jun 2021 16:19:30 +0200},
biburl = {https://dblp.org/rec/conf/icfp/MyreenO12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/Myreen12,
author = {Magnus O. Myreen},
editor = {Lennart Beringer and
Amy P. Felty},
title = {Functional Programs: Conversions between Deep and Shallow Embeddings},
booktitle = {Interactive Theorem Proving - Third International Conference, {ITP}
2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7406},
pages = {412--417},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-32347-8\_29},
doi = {10.1007/978-3-642-32347-8\_29},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/Myreen12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/MyreenD11,
author = {Magnus O. Myreen and
Jared Davis},
editor = {Marko C. J. D. van Eekelen and
Herman Geuvers and
Julien Schmaltz and
Freek Wiedijk},
title = {A Verified Runtime for a Verified Theorem Prover},
booktitle = {Interactive Theorem Proving - Second International Conference, {ITP}
2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6898},
pages = {265--280},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-22863-6\_20},
doi = {10.1007/978-3-642-22863-6\_20},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/MyreenD11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
url = {https://doi.org/10.1145/1785414.1785443},
doi = {10.1145/1785414.1785443},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/cacm/SewellSONM10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/FoxM10,
author = {Anthony C. J. Fox and
Magnus O. Myreen},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
title = {A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture},
booktitle = {Interactive Theorem Proving, First International Conference, {ITP}
2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {243--258},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_18},
doi = {10.1007/978-3-642-14052-5\_18},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/FoxM10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/Myreen10,
author = {Magnus O. Myreen},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
title = {Separation Logic Adapted for Proofs by Rewriting},
booktitle = {Interactive Theorem Proving, First International Conference, {ITP}
2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {485--489},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_34},
doi = {10.1007/978-3-642-14052-5\_34},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/Myreen10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/Myreen10,
author = {Magnus O. Myreen},
editor = {Manuel V. Hermenegildo and
Jens Palsberg},
title = {Verified just-in-time compiler on x86},
booktitle = {Proceedings of the 37th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
of Programming Languages, {POPL} 2010, Madrid, Spain, January 17-23,
2010},
pages = {107--118},
publisher = {{ACM}},
year = {2010},
url = {https://doi.org/10.1145/1706299.1706313},
doi = {10.1145/1706299.1706313},
timestamp = {Sat, 21 Oct 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/popl/Myreen10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vstte/Myreen10,
author = {Magnus O. Myreen},
editor = {Gary T. Leavens and
Peter W. O'Hearn and
Sriram K. Rajamani},
title = {Reusable Verification of a Copying Collector},
booktitle = {Verified Software: Theories, Tools, Experiments, Third International
Conference, {VSTTE} 2010, Edinburgh, UK, August 16-19, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6217},
pages = {142--156},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-15057-9\_10},
doi = {10.1007/978-3-642-15057-9\_10},
timestamp = {Tue, 14 May 2019 10:00:49 +0200},
biburl = {https://dblp.org/rec/conf/vstte/Myreen10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/sp/10/FoxGM10,
author = {Anthony C. J. Fox and
Michael J. C. Gordon and
Magnus O. Myreen},
editor = {David S. Hardin},
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},
url = {https://doi.org/10.1007/978-1-4419-1539-9\_8},
doi = {10.1007/978-1-4419-1539-9\_8},
timestamp = {Thu, 16 May 2019 21:02:15 +0200},
biburl = {https://dblp.org/rec/books/sp/10/FoxGM10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{DBLP:phd/ethos/Myreen09,
author = {Magnus Oskar Myreen},
title = {Formal verification of machine-code programs},
school = {University of Cambridge, {UK}},
year = {2009},
url = {https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.611450},
timestamp = {Tue, 05 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/phd/ethos/Myreen09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cc/MyreenSG09,
author = {Magnus O. Myreen and
Konrad Slind and
Michael J. C. Gordon},
editor = {Oege de Moor and
Michael I. Schwartzbach},
title = {Extensible Proof-Producing Compilation},
booktitle = {Compiler Construction, 18th International Conference, {CC} 2009, Held
as Part of the Joint European Conferences on Theory and Practice of
Software, {ETAPS} 2009, York, UK, March 22-29, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5501},
pages = {2--16},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-00722-4\_2},
doi = {10.1007/978-3-642-00722-4\_2},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/cc/MyreenSG09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
editor = {Leaf Petersen and
Manuel M. T. Chakravarty},
title = {The semantics of power and {ARM} multiprocessor machine code},
booktitle = {Proceedings of the {POPL} 2009 Workshop on Declarative Aspects of
Multicore Programming, {DAMP} 2009, Savannah, GA, USA, January 20,
2009},
pages = {13--24},
publisher = {{ACM}},
year = {2009},
url = {https://doi.org/10.1145/1481839.1481842},
doi = {10.1145/1481839.1481842},
timestamp = {Fri, 25 Jun 2021 14:48:54 +0200},
biburl = {https://dblp.org/rec/conf/popl/AlglaveFIMSSN09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@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},
editor = {Zhong Shao and
Benjamin C. Pierce},
title = {The semantics of x86-CC multiprocessor machine code},
booktitle = {Proceedings of the 36th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
of Programming Languages, {POPL} 2009, Savannah, GA, USA, January
21-23, 2009},
pages = {379--391},
publisher = {{ACM}},
year = {2009},
url = {https://doi.org/10.1145/1480881.1480929},
doi = {10.1145/1480881.1480929},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/popl/SarkarSNORBMA09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/MyreenG09,
author = {Magnus O. Myreen and
Michael J. C. Gordon},
editor = {Stefan Berghofer and
Tobias Nipkow and
Christian Urban and
Makarius Wenzel},
title = {Verified {LISP} Implementations on ARM, x86 and PowerPC},
booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference,
TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5674},
pages = {359--374},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-03359-9\_25},
doi = {10.1007/978-3-642-03359-9\_25},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/MyreenG09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/MyreenGS08,
author = {Magnus O. Myreen and
Michael J. C. Gordon and
Konrad Slind},
editor = {Alessandro Cimatti and
Robert B. Jones},
title = {Machine-Code Verification for Multiple Architectures - An Application
of Decompilation into Logic},
booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2008, Portland, Oregon,
USA, 17-20 November 2008},
pages = {1--8},
publisher = {{IEEE}},
year = {2008},
url = {https://doi.org/10.1109/FMCAD.2008.ECP.24},
doi = {10.1109/FMCAD.2008.ECP.24},
timestamp = {Wed, 16 Oct 2019 14:14:56 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/MyreenGS08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/MyreenG09,
author = {Magnus O. Myreen and
Michael J. C. Gordon},
editor = {Patr{\'{\i}}cia D. L. Machado},
title = {Transforming Programs into Recursive Functions},
booktitle = {Proceedings of the Eleventh Brazilian Symposium on Formal Methods,
{SBMF} 2008, Salvador, Brazil, August 26-29, 2008},
series = {Electronic Notes in Theoretical Computer Science},
volume = {240},
pages = {185--200},
publisher = {Elsevier},
year = {2008},
url = {https://doi.org/10.1016/j.entcs.2009.05.052},
doi = {10.1016/J.ENTCS.2009.05.052},
timestamp = {Thu, 09 Mar 2023 13:31:46 +0100},
biburl = {https://dblp.org/rec/journals/entcs/MyreenG09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fsen/MyreenFG07,
author = {Magnus O. Myreen and
Anthony C. J. Fox and
Michael J. C. Gordon},
editor = {Farhad Arbab and
Marjan Sirjani},
title = {Hoare Logic for {ARM} Machine Code},
booktitle = {International Symposium on Fundamentals of Software Engineering, International
Symposium, {FSEN} 2007, Tehran, Iran, April 17-19, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4767},
pages = {272--286},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-75698-9\_18},
doi = {10.1007/978-3-540-75698-9\_18},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/fsen/MyreenFG07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/MyreenG07,
author = {Magnus O. Myreen and
Michael J. C. Gordon},
editor = {Orna Grumberg and
Michael Huth},
title = {Hoare Logic for Realistically Modelled Machine Code},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
13th International Conference, {TACAS} 2007, Held as Part of the Joint
European Conferences on Theory and Practice of Software, {ETAPS} 2007
Braga, Portugal, March 24 - April 1, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4424},
pages = {568--582},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-71209-1\_44},
doi = {10.1007/978-3-540-71209-1\_44},
timestamp = {Mon, 11 Sep 2023 15:43:49 +0200},
biburl = {https://dblp.org/rec/conf/tacas/MyreenG07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tap/BackEM07,
author = {Ralph{-}Johan Back and
Johannes Eriksson and
Magnus Myreen},
editor = {Yuri Gurevich and
Bertrand Meyer},
title = {Testing and Verifying Invariant Based Programs in the {SOCOS} Environment},
booktitle = {Tests and Proofs - 1st International Conference, {TAP} 2007, Zurich,
Switzerland, February 12-13, 2007. Revised Papers},
series = {Lecture Notes in Computer Science},
volume = {4454},
pages = {61--78},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-73770-4\_4},
doi = {10.1007/978-3-540-73770-4\_4},
timestamp = {Tue, 23 Jun 2020 17:02:04 +0200},
biburl = {https://dblp.org/rec/conf/tap/BackEM07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/apsec/BackM05,
author = {Ralph{-}Johan Back and
Magnus Myreen},
title = {Tool Support for Invariant Based Programming},
booktitle = {12th Asia-Pacific Software Engineering Conference {(APSEC} 2005),
15-17 December 2005, Taipei, Taiwan},
pages = {711--718},
publisher = {{IEEE} Computer Society},
year = {2005},
url = {https://doi.org/10.1109/APSEC.2005.104},
doi = {10.1109/APSEC.2005.104},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/apsec/BackM05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
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-04-15 20:46 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:
