Magnus Myreen

Cited by

	All	Since 2019
Citations	3731	1985
h-index	30	24
i10-index	51	40

400

200

100

300

20072008200920102011201220132014201520162017201820192020202120222023202413 25 51 100 105 120 155 169 201 209 262 301 397 327 339 343 398 180

Public access

View all

28 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
Zachary TatlockUniversity of WashingtonVerified email at cs.washington.edu
Eva DarulovaUppsala UniversityVerified email at it.uu.se
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	562	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	518*
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	210	2009
Translation validation for a verified OS kernel TAL Sewell, MO Myreen, G Klein Proceedings of the 34th ACM SIGPLAN conference on Programming language …, 2013	209	2013
A trustworthy monadic formalization of the ARMv7 instruction set architecture A Fox, MO Myreen International Conference on Interactive Theorem Proving, 243-258, 2010	195	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	119	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	97	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	97	2016
Verified just-in-time compiler on x86 MO Myreen Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010	96	2010
Hoare logic for realistically modelled machine code MO Myreen, MJC Gordon International Conference on Tools and Algorithms for the Construction and …, 2007	92	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	86	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	82	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	77	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	60	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	58	2017
Decompilation into logic—improved MO Myreen, MJC Gordon, K Slind 2012 Formal Methods in Computer-Aided Design (FMCAD), 78-81, 2012	52	2012
Proof-producing synthesis of ML from higher-order logic MO Myreen, S Owens ACM SIGPLAN Notices 47 (9), 115-126, 2012	48	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	43	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