Trustworthy Systems

Michael Norrish
Adjunct Associate Professor; Associate Professor, ANU

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. Michael now is a Associate Professor at ANU.

Contact Details

Phone: +61 2 6218 3719
Email:Michael.Norrish@anu.edu.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.

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 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
Abstract
Slides
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
Best Paper Award
Hall of Fame Award
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


Trustworthy Systems Group Papers

2023

Abstract PDF Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Gordon Sau, Ben Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus Myreen, Michael Norrish and Gernot Heiser
Pancake: verified systems programming made sweeter
Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 2023
plain text to be published Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus Myreen, Michael Norrish, Johannes Åman Pohjola and Riccardo Zanetti
Purecake: A verified compiler for a lazy functional language
Proc. ACM Program. Lang., Volume 7, Number PLDI, pp. 952–976, 2023

2020

Abstract to be published Michael Norrish and Yiming Xu
Mechanised modal model theory
International Joint Conference on Automated Reasoning, pp. 518-533, Paris, July, 2020

2019

Abstract PDF Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus Myreen, Michael Norrish, Oskar Abrahamsson and Anthony Fox
Verified compilation on a verified processor
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1041-1053, Phoenix, Arizona, United States of America, June, 2019
Abstract PDF Hing-Lun Chan and Michael Norrish
Proof pearl: Bounding least common multiples with triangles
Journal of Automated Reasoning, Volume 62, Issue 2, pp. 171-192, February, 2019
Abstract PDF Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish
The verified CakeML compiler backend
Journal of Functional Programming, Volume 29, February, 2019
Abstract PDF Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith and Keith Wanbrough
Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the sockets API
Journal of the ACM, Volume 66, Issue 1, January, 2019

2018

Abstract PDF Milad Ghale, Dirk Pattinson, Ramana Kumar and Michael Norrish
Verified certificate checking for counting votes
Verified Software: Theories, Tools and Experiments, pp. 69–87, Oxford, December, 2018
Abstract PDF Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus Myreen, Yong Kiam Tan and Michael Norrish
Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
International Joint Conference on Automated Reasoning, pp. 646-662, Oxford, July, 2018
Abstract PDF Simon Jantsch and Michael Norrish
Verifying the LTL to Büchi automata translation via very weak alternating automata
International Conference on Interactive Theorem Proving, pp. 306-323, Oxford, July, 2018
Abstract PDF Kunshan Wang, Stephen Blackburn, Tony Hosking and Michael Norrish
Hop, skip, & jump: Practical on-stack replacement for a cross-platform language-neutral VM
International Conference on Virtual Execution Environments, pp. 1-16, Williamsburg, VA, March, 2018

2017

Abstract PDF Scott Owens, Michael Norrish, Ramana Kumar, Yong Kiam Tan and Magnus Myreen
Verifying efficient function calls in CakeML
International Conference on Functional Programming, Oxford, September, 2017
Abstract PDF Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish
Verified characteristic formulae for CakeML
European Symposium on Programming, pp. 584–610, Uppsala, Sweden, April, 2017
Abstract to be published Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish
Verified characteristic formulae for CakeML
European Symposium on Programming, pp. 584-610, Uppsala, April, 2017

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 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

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
International Joint Conference on Artificial Intelligence, 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
Slides
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
Slides
PDF Michael Norrish and Brian Huffman
Ordinals in HOL: Transfinite arithmetic up to (and beyond) $\omega_1$
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
Slides
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
Slides
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
Slides
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
Best Paper Award
Hall of Fame Award
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
European Symposium on Programming, 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
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
Slides
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
Slides
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

2018

Abstract PDF Mohammad Abdulaziz
Formally verified compositional algorithms for factored transition systems
PhD Thesis, Australian National University, June, 2018