Michael Norrish

Cited by

	All	Since 2016
Citations	4475	2092
h-index	24	15
i10-index	42	23

540

270

135

405

200020012002200320042005200620072008200920102011201220132014201520162017201820192020202118 27 36 35 21 60 81 75 104 130 247 237 262 279 301 373 349 368 432 521 408 13

Co-authors

Ramana KumarDeepMindVerified email at cl.cam.ac.uk
Gerwin KleinData61 and UNSWVerified email at cse.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 Sydney, and Data61, CSIROVerified email at unsw.edu.au
Scott OwensUniversity of KentVerified email at kent.ac.uk
Kevin ElphinstoneUniversity of New South WalesVerified email at cse.unsw.edu.au
Kai Engelhardtghost locomotiveVerified email at gh.st
Yong Kiam TanGraduate Research Assistant, CMUVerified email at cs.cmu.edu
Charles GrettonThe Australian National UniversityVerified email at anu.edu.au
Tony HoskingAustralian National University, Data61Verified email at anu.edu.au
Mohammad AbdulazizTechnical University of MunichVerified email at in.tum.de
Tom RidgeDepartment of Informatics, University of LeicesterVerified email at le.ac.uk
Steve BlackburnProfessor of Computer Science, Australian National UniversityVerified email at anu.edu.au
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
James CheneyReader, Laboratory for Foundations of Computer Science, University of EdinburghVerified email at inf.ed.ac.uk
Michelle Mills StroutProfessor of Computer Science, University of ArizonaVerified email at cs.arizona.edu

Michael Norrish

Principal Research Scientist, Data61

Verified email at data61.csiro.au - Homepage

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	2091	2009
A brief overview of HOL4 K Slind, M Norrish International Conference on Theorem Proving in Higher Order Logics, 28-32, 2008	305	2008
CakeML: a verified implementation of ML R Kumar, MO Myreen, M Norrish, S Owens ACM SIGPLAN Notices 49 (1), 179-191, 2014	292	2014
C formalised in HOL M Norrish University of Cambridge, Computer Laboratory, 1998	250	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	220	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	112	2005
The PROSPER toolkit LA Dennis, G Collins, M Norrish, R Boulton, K Slind, G Robinson, ... International Conference on Tools and Algorithms for the Construction and …, 2000	110	2000
Barendregt’s variable convention in rule inductions C Urban, S Berghofer, M Norrish International Conference on Automated Deduction, 35-50, 2007	79	2007
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	76	2016
Learning to Reason with HOL4 tactics T Gauthier, C Kaliszyk, J Urban arXiv preprint arXiv:1804.00595, 2018	65*	2018
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	58	2006
Mind the gap S Winwood, G Klein, T Sewell, J Andronick, D Cock, M Norrish International Conference on Theorem Proving in Higher Order Logics, 500-515, 2009	54	2009
Recursive function definition for types with binders M Norrish International Conference on Theorem Proving in Higher Order Logics, 241-256, 2004	37	2004
Deterministic expressions in C M Norrish European Symposium on Programming, 147-161, 1999	34	1999
Mechanised computability theory M Norrish International Conference on Interactive Theorem Proving, 297-311, 2011	32	2011
The PROSPER toolkit LA Dennis, G Collins, M Norrish, RJ Boulton, K Slind, TF Melham International Journal on Software Tools for Technology Transfer 4 (2), 189-210, 2003	32	2003
Verified characteristic formulae for CakeML A Guéneau, MO Myreen, R Kumar, M Norrish European Symposium on Programming, 584-610, 2017	30	2017
Verified, executable parsing A Barthwal, M Norrish European Symposium on Programming, 160-174, 2009	30	2009
The verified CakeML compiler backend YK Tan, MO Myreen, R Kumar, A Fox, S Owens, M Norrish Journal of Functional Programming 29, 2019	26	2019
Complete integer decision procedures as derived rules in HOL M Norrish International Conference on Theorem Proving in Higher Order Logics, 71-86, 2003	25	2003

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

Upload PDF

Follow this author

Cited by

Co-authors