Michael Norrish

Cited by

	All	Since 2018
Citations	5394	2250
h-index	25	17
i10-index	46	26

520

260

130

390

20002001200220032004200520062007200820092010201120122013201420152016201720182019202020212022202314 31 40 34 23 61 75 76 112 127 245 232 271 277 314 376 371 370 454 512 386 443 420 35

Public access

View all

30 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Ramana KumarDeepMindVerified email at cl.cam.ac.uk
Peter SewellComputer Laboratory, University of CambridgeVerified email at cl.cam.ac.uk
Gerwin KleinProofcraft and UNSWVerified email at unsw.edu.au
Magnus MyreenChalmers University of TechnologyVerified email at cl.cam.ac.uk
David CockGraduate Researcher, NICTA and University of New South WalesVerified email at cse.unsw.edu.au
June AndronickPrincipal Research Scientist, Data61, CSIROVerified email at data61.csiro.au
Gernot HeiserProfessor of Computer Science, UNSW SydneyVerified email at unsw.edu.au
Scott OwensUniversity of KentVerified email at kent.ac.uk
Yong Kiam TanScientist I, Institute for Infocomm Research, SingaporeVerified email at cs.cmu.edu
Tony HoskingAustralian National University, Data61Verified email at anu.edu.au
Kevin ElphinstoneUniversity of New South WalesVerified email at cse.unsw.edu.au
Kai Engelhardtn.a.Verified email at acm.org
Dhammika ElkaduweUniversity of Peradeniya (www.pdn.ac.lk)Verified email at ce.pdn.ac.lk
Charles GrettonThe Australian National UniversityVerified email at anu.edu.au
Mohammad AbdulazizTechniche Universität MünchenVerified email at in.tum.de
Steve BlackburnResearch Scientist, Google | Professor of Computer Science, Australian National UniversityVerified email at google.com
Tom RidgeIndependentVerified email at tom-ridge.com
Christian UrbanKing's College LondonVerified email at kcl.ac.uk
Tom MelhamProfessor of Computer Science, University of OxfordVerified email at cs.ox.ac.uk
Louise DennisDepartment of Computer Science, University of ManchesterVerified email at manchester.ac.uk

Michael Norrish

Australian National University

Verified email at anu.edu.au

Formal Methods Interactive Theorem Proving


Title Sort by citations Sort by year Sort by title	Cited by Cited by	Year
seL4: Formal verification of an OS kernel G Klein, K Elphinstone, G Heiser, J Andronick, D Cock, P Derrin, ... Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles …, 2009	2535	2009
CakeML: a verified implementation of ML R Kumar, MO Myreen, M Norrish, S Owens ACM SIGPLAN Notices 49 (1), 179-191, 2014	420	2014
A brief overview of HOL4 K Slind, M Norrish Theorem Proving in Higher Order Logics: 21st International Conference …, 2008	381	2008
C formalised in HOL M Norrish University of Cambridge, Computer Laboratory, 1998	279	1998
Types, bytes, and separation logic H Tuch, G Klein, M Norrish Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2007	232	2007
Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets S Bishop, M Fairbairn, M Norrish, P Sewell, M Smith, K Wansbrough Proceedings of the 2005 conference on Applications, technologies …, 2005	126	2005
The PROSPER toolkit LA Dennis, G Collins, M Norrish, R Boulton, K Slind, G Robinson, ... Tools and Algorithms for the Construction and Analysis of Systems: 6th …, 2000	113	2000
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
Barendregt’s variable convention in rule inductions C Urban, S Berghofer, M Norrish Automated Deduction–CADE-21: 21st International Conference on Automated …, 2007	84	2007
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations S Bishop, M Fairbairn, M Norrish, P Sewell, M Smith, K Wansbrough Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of …, 2006	66	2006
Mind the gap: A verification framework for low-level C S Winwood, G Klein, T Sewell, J Andronick, D Cock, M Norrish Theorem Proving in Higher Order Logics: 22nd International Conference …, 2009	63	2009
The verified CakeML compiler backend YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish Journal of Functional Programming 29, e2, 2019	54	2019
Verified characteristic formulae for CakeML A Guéneau, MO Myreen, R Kumar, M Norrish Programming Languages and Systems: 26th European Symposium on Programming …, 2017	41	2017
Mechanised computability theory M Norrish Interactive Theorem Proving: Second International Conference, ITP 2011, Berg …, 2011	39	2011
Recursive function definition for types with binders M Norrish Theorem Proving in Higher Order Logics: 17th International Conference …, 2004	38	2004
Deterministic expressions in C M Norrish Programming Languages and Systems: 8th European Symposium on Programming …, 2002	37	2002
TacticToe: learning to prove with tactics T Gauthier, C Kaliszyk, J Urban, R Kumar, M Norrish Journal of Automated Reasoning 65, 257-286, 2021	36*	2021
Verified, executable parsing A Barthwal, M Norrish Programming Languages and Systems: 18th European Symposium on Programming …, 2009	36	2009
The PROSPER toolkit LA Dennis, G Collins, M Norrish, RJ Boulton, K Slind, TF Melham International Journal on Software Tools for Technology Transfer 4, 189-210, 2003	33	2003
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	29	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