Michael Norrish

Cited by

	All	Since 2018
Citations	5858	2711
h-index	25	19
i10-index	50	29

540

270

135

405

20002001200220032004200520062007200820092010201120122013201420152016201720182019202020212022202315 27 35 36 24 60 76 75 108 128 249 229 266 280 314 376 368 377 452 534 381 451 433 458

Public access

View all

32 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Ramana KumarDeepMindVerified email at cl.cam.ac.uk
Magnus MyreenChalmers University of TechnologyVerified 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
David CockSenior Researcher, ETH ZurichVerified email at cse.unsw.edu.au
Gernot HeiserProfessor of Computer Science, University of New South WalesVerified email at unsw.edu.au
June AndronickCEO and co-founcer, ProofcraftVerified email at proofcraft.systems
Scott OwensUniversity of KentVerified email at kent.ac.uk
Tony HoskingAustralian National UniversityVerified email at anu.edu.au
Yong Kiam TanScientist I, Institute for Infocomm Research, SingaporeVerified email at cs.cmu.edu
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 Gretton, FIEAustThe Australian National UniversityVerified email at anu.edu.au
Mohammad AbdulazizKing's College LondonVerified 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 - 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	2709	2009
CakeML: a verified implementation of ML R Kumar, MO Myreen, M Norrish, S Owens ACM SIGPLAN Notices 49 (1), 179-191, 2014	482	2014
A brief overview of HOL4 K Slind, M Norrish International Conference on Theorem Proving in Higher Order Logics, 28-32, 2008	412	2008
C formalised in HOL M Norrish University of Cambridge, Computer Laboratory, 1998	287	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	236	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	131	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	112	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	97	2016
Barendregt’s variable convention in rule inductions C Urban, S Berghofer, M Norrish Automated Deduction–CADE-21: 21st International Conference on Automated …, 2007	85	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	72	2019
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	68	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
Seed selection for successful fuzzing A Herrera, H Gunadi, S Magrath, M Norrish, M Payer, AL Hosking Proceedings of the 30th ACM SIGSOFT international symposium on software …, 2021	58	2021
TacticToe: learning to prove with tactics T Gauthier, C Kaliszyk, J Urban, R Kumar, M Norrish Journal of Automated Reasoning 65, 257-286, 2021	55*	2021
Verified characteristic formulae for CakeML A Guéneau, MO Myreen, R Kumar, M Norrish Programming Languages and Systems: 26th European Symposium on Programming …, 2017	53	2017
Mechanised computability theory M Norrish Interactive Theorem Proving: Second International Conference, ITP 2011, Berg …, 2011	44	2011
Recursive function definition for types with binders M Norrish International Conference on Theorem Proving in Higher Order Logics, 241-256, 2004	39	2004
Deterministic expressions in C M Norrish European Symposium on Programming, 147-161, 1999	38	1999
Verified, executable parsing A Barthwal, M Norrish Programming Languages and Systems: 18th European Symposium on Programming …, 2009	37	2009
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	36	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