Magnus Myreen

Cited by

	All	Since 2019
Citations	3867	2107
h-index	30	25
i10-index	52	41

400

200

100

300

20072008200920102011201220132014201520162017201820192020202120222023202413 25 51 101 104 120 154 170 203 211 262 301 397 326 341 345 397 298

Public access

View all

29 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Ramana KumarDeepMindVerified email at cl.cam.ac.uk
Scott OwensUniversity of KentVerified email at kent.ac.uk
Yong Kiam TanInstitute 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 SarkarProfessor of Computer Science, University of St AndrewsVerified email at st-andrews.ac.uk
Peter SewellComputer Laboratory, University of CambridgeVerified email at cl.cam.ac.uk
Johannes Åman PohjolaUniversity of New South WalesVerified email at unsw.edu.au
Jade AlglaveARM and University College LondonVerified email at ucl.ac.uk
Tom RidgeIndependentVerified email at tom-ridge.com
Marijn HeuleAssociate Professor of Computer Science, Carnegie Mellon UniversityVerified email at cs.cmu.edu
Ralph-Johan BackProfessor of Computer Science, Åbo AkademiVerified email at abo.fi
Gerwin KleinProofcraft and UNSWVerified email at unsw.edu.au
Eva DarulovaUppsala UniversityVerified email at it.uu.se
Zachary TatlockUniversity of WashingtonVerified email at cs.washington.edu
Samin IshtiaqRiverlaneVerified email at riverlane.com
Hira Taqdees SyedaApplied Sceintist II, Amazon Web ServicesVerified email at amazon.com
Rose BohrerAssistant Professor, Worcester Polytechnic InstituteVerified email at wpi.edu
Stefan MitschSchool of Computing, DePaul UniversityVerified email at depaul.edu
André PlatzerAlexander von Humboldt Professor, Karlsruhe Institute of TechnologyVerified email at kit.edu

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	582	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	547*
Translation validation for a verified OS kernel TAL Sewell, MO Myreen, G Klein Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013	222	2013
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	212	2009
A trustworthy monadic formalization of the ARMv7 instruction set architecture A Fox, MO Myreen International Conference on Interactive Theorem Proving, 243-258, 2010	196	2010
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	147	2009
Functional big-step semantics S Owens, MO Myreen, R Kumar, YK Tan Programming Languages and Systems: 25th European Symposium on Programming …, 2016	121	2016
VeriPhy: verified controller executables from verified cyber-physical system models R Bohrer, YK Tan, S Mitsch, MO Myreen, A Platzer Proceedings of the 39th ACM SIGPLAN Conference on Programming Language …, 2018	102	2018
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	99	2016
Verified just-in-time compiler on x86 MO Myreen Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010	99	2010
Hoare logic for realistically modelled machine code MO Myreen, MJC Gordon International Conference on Tools and Algorithms for the Construction and …, 2007	95	2007
The verified CakeML compiler backend YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish Journal of Functional Programming 29, e2, 2019	91	2019
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	84	2008
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	78	2014
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	68	2016
Formal verification of machine-code programs MO Myreen British Computer Society, 2011	61	2011
Verified characteristic formulae for CakeML A Guéneau, MO Myreen, R Kumar, M Norrish European Symposium on Programming (ESOP), Springer, Lecture Notes in …, 2017	60	2017
Decompilation into logic—improved MO Myreen, MJC Gordon, K Slind 2012 Formal Methods in Computer-Aided Design (FMCAD), 78-81, 2012	53	2012
Proof-producing synthesis of ML from higher-order logic MO Myreen, S Owens ACM SIGPLAN Notices 47 (9), 115-126, 2012	50	2012
Verified compilation on a verified processor A Lööw, R Kumar, YK Tan, MO Myreen, M Norrish, O Abrahamsson, A Fox Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019	47	2019

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