Magnus Myreen

Cited by

	All	Since 2018
Citations	3202	1752
h-index	27	22
i10-index	47	38

400

200

100

300

2007200820092010201120122013201420152016201720182019202020212022202312 25 51 99 105 122 148 172 207 212 267 301 383 330 325 346 65

Public access

View all

22 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Scott OwensUniversity of KentVerified email at kent.ac.uk
Ramana KumarDeepMindVerified email at cl.cam.ac.uk
Yong Kiam TanScientist I, Institute for Infocomm Research, SingaporeVerified email at cs.cmu.edu
Michael NorrishAustralian National UniversityVerified email at anu.edu.au
Francesco Zappa NardelliFacebookVerified email at fb.com
Susmit SarkarReader, University of St AndrewsVerified email at st-andrews.ac.uk
Peter SewellComputer Laboratory, University of CambridgeVerified email at cl.cam.ac.uk
Jade AlglaveARM and University College LondonVerified email at ucl.ac.uk
Tom RidgeIndependentVerified email at tom-ridge.com
Johannes Åman PohjolaUniversity of New South WalesVerified email at unsw.edu.au
Ralph-Johan BackProfessor of Computer Science, Åbo AkademiVerified email at abo.fi
Gerwin KleinProofcraft and UNSWVerified email at unsw.edu.au
Zachary TatlockUniversity of WashingtonVerified email at cs.washington.edu
Samin IshtiaqRiverlaneVerified email at riverlane.com
Marijn HeuleAssociate Professor of Computer Science, Carnegie Mellon UniversityVerified email at cs.cmu.edu
Eva DarulovaUppsala UniversityVerified email at it.uu.se
Rose BohrerAssistant Professor, Worcester Polytechnic InstituteVerified email at wpi.edu
Stefan MitschComputer Science Department, Carnegie Mellon UniversityVerified email at cs.cmu.edu
André PlatzerAlexander von Humboldt Professor of Computer Science, Karlsruhe Institute of TechnologyVerified email at kit.edu
Nikita ZyuzinIMDEA Software InstituteVerified email at imdea.org

Magnus Myreen

Chalmers University of Technology

Verified email at cl.cam.ac.uk - Homepage

Formal Verification Functional Programming Interactive Theorem Proving Computer Science


Title Sort by citations Sort by year Sort by title	Cited by Cited by	Year
x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors P Sewell, S Sarkar, S Owens, FZ Nardelli, MO Myreen Communications of the ACM 53 (7), 89-97, 2010	514	2010
CakeML: A Verified Implementation of ML R Kumar, MO Myreen, SA Owens, M Norrish ACM Symposium on Principles of Programming Languages (POPL) 2014, 0	427*
The semantics of x86-CC multiprocessor machine code S Sarkar, P Sewell, FZ Nardelli, S Owens, T Ridge, T Braibant, ... ACM SIGPLAN Notices 44 (1), 379-391, 2009	194	2009
A trustworthy monadic formalization of the ARMv7 instruction set architecture A Fox, MO Myreen Interactive Theorem Proving: First International Conference, ITP 2010 …, 2010	182	2010
Translation validation for a verified OS kernel TAL Sewell, MO Myreen, G Klein Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013	179	2013
The semantics of Power and ARM multiprocessor machine code J Alglave, A Fox, S Ishtiaq, MO Myreen, S Sarkar, P Sewell, FZ Nardelli Proceedings of the 4th workshop on Declarative aspects of multicore …, 2009	143	2009
Functional big-step semantics S Owens, MO Myreen, R Kumar, YK Tan Programming Languages and Systems: 25th European Symposium on Programming …, 2016	104	2016
A new verified compiler backend for CakeML YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish Proceedings of the 21st ACM SIGPLAN International Conference on Functional …, 2016	92	2016
Verified just-in-time compiler on x86 MO Myreen Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010	91	2010
Hoare logic for realistically modelled machine code MO Myreen, MJC Gordon Tools and Algorithms for the Construction and Analysis of Systems: 13th …, 2007	82	2007
Machine-code verification for multiple architectures-an application of decompilation into logic MO Myreen, MJC Gordon, K Slind 2008 Formal Methods in Computer-Aided Design, 1-8, 2008	75	2008
VeriPhy: verified controller executables from verified cyber-physical system models B Bohrer, YK Tan, S Mitsch, MO Myreen, A Platzer Proceedings of the 39th ACM SIGPLAN Conference on Programming Language …, 2018	67	2018
Proof-producing translation of higher-order logic into pure and stateful ML MO Myreen, S Owens Journal of Functional Programming 24 (2-3), 284-315, 2014	66	2014
Formal verification of machine-code programs MO Myreen British Computer Society, 2011	62	2011
Self-formalisation of higher-order logic: Semantics, soundness, and a verified implementation R Kumar, R Arthan, MO Myreen, S Owens Journal of Automated Reasoning 56, 221-259, 2016	60	2016
The verified CakeML compiler backend YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish Journal of Functional Programming 29, e2, 2019	56	2019
Decompilation into logic—improved MO Myreen, MJC Gordon, K Slind 2012 Formal Methods in Computer-Aided Design (FMCAD), 78-81, 2012	49	2012
Verified characteristic formulae for CakeML A Guéneau, MO Myreen, R Kumar, M Norrish European Symposium on Programming (ESOP), Springer, Lecture Notes in …, 2017	44	2017
A verified runtime for a verified theorem prover MO Myreen, J Davis Interactive Theorem Proving: Second International Conference, ITP 2011, Berg …, 2011	40	2011
HOL with Definitions: Semantics, Soundness, and a Verified Implementation R Kumar, R Arthan, MO Myreen, S Owens Interactive Theorem Proving: Fifth International Conference, ITP 2014, 2014	39	2014

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Follow

Cited by

Co-authors