Skip to main content

Michael Norrish

Michael Norrish
Principal Researcher

Research Interests

Michael is interested in the use of mathematics and logic to help in the specification and development of computer hardware and software. He is interested both in working on specific applications projects in this area, and in the development of tools to make all such projects easier to work on.

Contact Details

Phone: +61 2 6218 3719
Email:Michael.Norrish@data61.csiro.au

More contact information is available at the Contact page.

Photo of Michael Norrish

Publication List


Michael is interested in the use of mathematics and logic to help in the specification and development of computer hardware and software. He is interested both in working on specific applications projects in this area, and in the development of tools to make all such projects easier to work on.

Projects

Current

Past

Qualifications

PhD [University of Cambridge, 1999]; BSc(Hons) [Victoria University of Wellington, 1993]; BA, BSc [Victoria University of Wellington, 1992]

Steering Committees

Interactive Theorem Proving, Certified Programs and Proofs

Program Committees and Editorial Boards

PLDI 2015 ITP 2014 CPP 2013 ITP 2013 ESOP 2013 EMSOFT 2012 CAV 2011 CPP 2011 ITP 2011 ITP 2010 TPHOLs 2009 LICS 2008

Publications

Best Papers

Abstract PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207-220, Big Sky, MT, USA, October, 2009
Abstract PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97-108, Nice, France, January, 2007


Data61 Papers

2016

Abstract PDF Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish
A new verified compiler backend for CakeML
International Conference on Functional Programming, pp. 14, Nara, Japan, September, 2016
Abstract PDF Joseph Chan and Michael Norrish
Proof pearl: Bounding least common multiples with triangles
International Conference on Interactive Theorem Proving, pp. 140–150, Nancy, France, August, 2016
Abstract PDF Yi Lin, Steve Blackburn, Tony Hosking and Michael Norrish
Rust as a language for high performance GC implementation
International Symposium on Memory Management, pp. 89-98, Santa Barbara, California, USA, June, 2016

NICTA Papers

2015

Abstract PDF Mohammad Abdulaziz, Charles Gretton and Michael Norrish
Verified over-approximation of the diameter of propositionally factored transition systems
International Conference on Interactive Theorem Proving, pp. 1-16, Nanjing, China, August, 2015
Abstract PDF Joseph Chan and Michael Norrish
Mechanisation of AKS algorithm: Part 1 – the main theorem
International Conference on Interactive Theorem Proving, pp. 117-136, Nanjing, China, August, 2015
Abstract PDF Mohammad Abdulaziz, Charles Gretton and Michael Norrish
Exploiting symmetries by planning for a descriptive quotient
IJCAI 2015, pp. 1479-1486, Buenos Aires, July, 2015
Abstract PDF Yi Lin, Stephen M. Blackburn, Kunshan Wang, Tony Hosking and Michael Norrish
Stop and go: Understanding yieldpoint behavior
International Symposium on Memory Management, pp. 70–80, Portland, OR, USA, June, 2015
Abstract PDF Michael Norrish and Michelle Mills Strout
An approach for proving the correctness of inspector/executor transformations
Languages and Compilers for Parallel Computing, pp. 131–145, Hillsboro, Oregon, USA, May, 2015
Abstract PDF Kunshan Wang, Yi Lin, Stephen M Blackburn, Michael Norrish and Tony Hosking
Draining the swamp: Micro virtual machines as a solid foundation for language development
SNAPL, pp. 321–336, Asilomar, California, May, 2015

2014

Abstract PDF Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish
Beagle as a HOL4 external ATP method
Practical Aspects of Automated Reasoning, pp. 50-59, Vienna, July, 2014
Abstract PDF Mohammad Abdulaziz, Charles Gretton and Michael Norrish
Mechanising theoretical upper bounds in planning
Workshop on Knowledge Engineering for Planning and Scheduling, Portsmouth, USA, June, 2014
Abstract PDF Aditi Barthwal and Michael Norrish
A mechanisation of some context-free language theory in HOL4
Journal of Computer and System Sciences, Volume 80, Number 2, pp. 346–362, March, 2014
Abstract PDF Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens
CakeML: A verified implementation of ML
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191, San Diego, January, 2014

2013

Abstract PDF Joseph Chan and Michael Norrish
A string of pearls: Proofs of fermat's little theorem
Journal of Formal Reasoning, Volume 6, Number 1, pp. 63–87, December, 2013
Abstract PDF Andreas Bauer, Peter Baumgartner, Diller Martin and Michael Norrish
Tableaux for verification of data-centric processes
Automated Reasoning with Analytic Tableaux and Related Methods, pp. 28-43, Nancy, France, September, 2013
Abstract PDF Michael Norrish and Brian Huffman
Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁
International Conference on Interactive Theorem Proving, pp. 133-146, Rennes, France, July, 2013

2012

Abstract PDF Hing-Lun Chan and Michael Norrish
A string of pearls: Proofs of fermat’s little theorem
International Conference on Certified Programs and Proofs, pp. 188-207, Kyoto, Japan, October, 2012
Abstract PDF James Cheney, Michael Norrish and René Vestergaard
Formalizing adequacy: A case study for higher-order abstract syntax
Journal of Automated Reasoning, Volume 49, Number 2, pp. 209–239, August, 2012

2011

Abstract PDF Michael Norrish
Mechanised computability theory
International Conference on Interactive Theorem Proving, pp. 297–311, Nijmegen, The Netherlands, August, 2011

2010

Abstract PDF Aditi Barthwal and Michael Norrish
A formalisation of the normal forms of context-free grammars in HOL4
19th EACSL Annual Conferences on Computer Science Logic, pp. 95-109, Brno, Czech Republic, August, 2010
Abstract PDF Aditi Barthwal and Michael Norrish
Mechanisation of PDA and grammar equivalence for context-free languages
17th Workshop on Logic, Language, Information and Computation , pp. 125-135, Brasília, Brazil, July, 2010
Abstract PDF Ramana Kumar and Michael Norrish
(nominal) unification by recursive descent with triangular substitutions
International Conference on Interactive Theorem Proving, pp. 51-66, Edinburgh, United Kingdom, July, 2010
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an operating-system kernel
Communications of the ACM, Volume 53, Number 6, pp. 107-115, June, 2010
Research Highlights paper

2009

Abstract PDF
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207-220, Big Sky, MT, USA, October, 2009
Abstract PDF Michael Norrish
Rewriting conversions implemented with continuations
Journal of Automated Reasoning, Volume 43, Number 3, pp. 305-336, October, 2009
Abstract PDF Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish
Mind the gap: A verification framework for low-level C
International Conference on Theorem Proving in Higher Order Logics, pp. 500-515, Munich, Germany, August, 2009
Abstract PDF Aditi Barthwal and Michael Norrish
Verified, executable parsing
ESOP, pp. 160-174, York, March, 2009
Abstract PDF James Cheney, René Vestergaard and Michael Norrish
Formalizing adequacy
2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming, York, March, 2009

2008

Abstract PDF Konrad Slind and Michael Norrish
A brief overview of HOL4
International Conference on Theorem Proving in Higher Order Logics, pp. 28-32, Montréal, Canada, August, 2008
Abstract PDF Tom Ridge, Michael Norrish and Peter Sewell
A rigorous approach to networking: TCP, from implementation to protocol to service
International Symposium on Formal Methods (FM), pp. 294–309, Turku, Finland, May, 2008

2007

Abstract PDF Michael Norrish
A formal semantics for c++
Technical Report, NICTA, November, 2007
Abstract PDF Michael Norrish and René Vestergaard
Proof pearl: de bruijn terms really do work
International Conference on Theorem Proving in Higher Order Logics, pp. 207-222, Kaiserslautern, September, 2007
Abstract PDF Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser
Verifying a high-performance micro-kernel
7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007
Abstract PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97-108, Nice, France, January, 2007

2006

Abstract PDF Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 55–66, Charleston, South Carolina, USA, January, 2006

2005

Abstract PDF Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough
Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets
ACM Conference on Communications, pp. 265–276, Philadelphia, August, 2005

2004

Abstract PDF Michael Norrish
Recursive function definition for types with binders
International Conference on Theorem Proving in Higher Order Logics, pp. 241–256, Park City, Utah, United States, September, 2004

2003

Abstract PDF Michael Norrish
Complete integer decision procedures as derived rules in HOL
International Conference on Theorem Proving in Higher Order Logics, pp. 71-86, Rome, September, 2003

Research Theses Supervised

2011

Abstract PDF Aditi Barthwal
A formalisation of the theory of context-free languages in higher order logic
PhD Thesis, College of Engineering and Computer Science, ANU, Canberra, Australia, July, 2011