Michael Norrish

View Scopus Profile

Dr Michael Norrish

Associate Professor

 https://orcid.org/0000-0003-1163-8467
Calculated based on number of publications stored in Pure and citations from Scopus
Calculated based on number of publications stored in Pure and citations from Scopus
Calculated based on number of publications stored in Pure and citations from Scopus
20042024

Research activity per year

  • 35 Conference contribution
  • 16 Article
  • 2 Chapter
  • 1 Conference article
Filter
Conference contribution

Search results

  • 2021

    On the formalisation of Kolmogorov complexity

    Catt, E. & Norrish, M., 17 Jan 2021, CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. Hritcu, C. & Popescu, A. (eds.). Association for Computing Machinery, Inc, p. 291-299 9 p. (CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    4 Citations (Scopus)

  • Seed selection for successful fuzzing

    Herrera, A., Gunadi, H., Magrath, S., Norrish, M., Payer, M. & Hosking, A. L., 11 Jul 2021, Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis: ISSTA 2021. Cadar, C. & Zhang, X. (eds.). Association for Computing Machinery, Inc, p. 230-243 3464795

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    49 Citations (Scopus)
  • 2020

    Mechanised Modal Model Theory

    Xu, Y. & Norrish, M., 2020, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings. Peltier, N. & Sofronie-Stokkermans, V. (eds.). Springer, p. 518-533 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12166 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    3 Citations (Scopus)
  • 2019

    A Verified Compositional Algorithm for AI Planning

    Mansour (Abdulaziz), M., Gretton, C. & Norrish, M., 2019, 10th International Conference on Interactive Theorem Proving (ITP 2019). J. H. J. OL. A. A. T. (ed.). USA: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, p. 1-19

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

  • Verified compilation on a verified processor

    Lööw, A., Kumar, R., Tan, Y. K., Myreen, M. O., Norrish, M., Abrahamsson, O. & Fox, A., 8 Jun 2019, PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. McKinley, K. S. & Fisher, K. (eds.). Association for Computing Machinery, p. 1041-1053 13 p. (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    20 Citations (Scopus)
  • 2018

    Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions

    Ho, S., Abrahamsson, O., Kumar, R., Myreen, M. O., Tan, Y. K. & Norrish, M., 2018, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Sebastiani, R., Galmiche, D. & Schulz, S. (eds.). Springer Verlag, p. 646-662 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    13 Citations (Scopus)

  • Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata

    Jantsch, S. & Norrish, M., 2018, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Avigad, J. & Mahboubi, A. (eds.). Springer Verlag, p. 306-323 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10895 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    2 Citations (Scopus)
  • 2017

    A state-space acyclicity property for exponentially tighter plan length bounds

    Abdulaziz, M., Gretton, C. & Norrish, M., 2017, Proceedings of the 27th International Conference on Automated Planning and Scheduling, ICAPS 2017. Barbulescu, L., Smith, S. F., Mausam & Frank, J. D. (eds.). AAAI Press, p. 2-10 9 p. (Proceedings International Conference on Automated Planning and Scheduling, ICAPS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    9 Citations (Scopus)

  • Verified characteristic formulae for CakeML

    Guéneau, A., Myreen, M. O., Kumar, R. & Norrish, M., 2017, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. Yang, H. (ed.). Springer Verlag, p. 584-610 27 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10201 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    30 Citations (Scopus)
  • 2016

    A new verified compiler backend for CakeML

    Tan, Y. K., Myreen, M., Kumar, R., Fox, A., Owens, S. & Norrish, M., 2016, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. J. G. G. K. (ed.). 1 ed. USA: Association for Computing Machinery (ACM), p. 60–73

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

  • Proof pearl: Bounding least common multiples with triangles

    Chan, H. L. & Norrish, M., 2016, Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. Blanchette, J. C. & Merz, S. (eds.). Springer Verlag, p. 140-150 11 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9807 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    3 Citations (Scopus)

  • Rust as a language for high performance GC implementation

    Lin, Y., Blackurn, S. M., Hosking, A. L. & Norrish, M., 14 Jun 2016, ISMM 2016 - Proceedings of the 2016 ACM SIGPLAN International Symposium on Memory Management, co-located with PLDI 2016. Flood, C. H. & Zhang, Z. (eds.). Association for Computing Machinery, p. 89-98 10 p. (International Symposium on Memory Management, ISMM; vol. 14-June-2016).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    8 Citations (Scopus)
  • 2015

    An approach for proving the correctness of inspector/executor transformations

    Norrish, M. & Strout, M. M., 2015, Languages and Compilers for Parallel Computing - 27th International Workshop, LCPC 2014, Revised Selected Papers. Brodman, J. & Tu, P. (eds.). Springer Verlag, p. 131-145 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8967).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    2 Citations (Scopus)

  • Draining the swamp: Micro virtual machines as solid foundation for language development

    Wang, K., Lin, Y., Blackburn, S. M., Norrish, M. & Hosking, A. L., 1 May 2015, 1st Summit on Advances in Programming Languages, SNAPL 2015. Ball, T., Bodik, R., Lerner, B. S., Morrisett, G. & Krishnamurthi, S. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, p. 321-336 16 p. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 32).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    9 Citations (Scopus)

  • Exploiting symmetries by planning for a descriptive quotient

    Abdulaziz, M., Norrish, M. & Gretton, C., 2015, IJCAI 2015 - Proceedings of the 24th International Joint Conference on Artificial Intelligence. Wooldridge, M. & Yang, Q. (eds.). International Joint Conferences on Artificial Intelligence, p. 1479-1486 8 p. (IJCAI International Joint Conference on Artificial Intelligence; vol. 2015-January).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    5 Citations (Scopus)

  • Mechanisation of AKS algorithm: Part 1 – The main theorem

    Chan, H. L. & Norrish, M., 2015, Interactive Theorem Proving - 6th International Conference, ITP 2015, Proceedings. Zhang, X. & Urban, C. (eds.). Springer Verlag, p. 117-136 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9236).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    8 Citations (Scopus)

  • Stop and go: Understanding yieldpoint behavior

    Lin, Y., Wang, K., Blackurn, S. M., Hosking, A. L. & Norrish, M., 14 Jun 2015, ISMM 2015 - Proceedings of the 2015 ACM SIGPLAN International Symposium on Memory Management, co-located with PLDI 2015. Bond, M. & Hosking, A. L. (eds.). Association for Computing Machinery, p. 70-80 11 p. (International Symposium on Memory Management, ISMM; vol. 14-June-2015).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    7 Citations (Scopus)

  • Verified over-approximation of the diameter of propositionally factored transition systems

    Abdulaziz, M., Gretton, C. & Norrish, M., 2015, Interactive Theorem Proving - 6th International Conference, ITP 2015, Proceedings. Zhang, X. & Urban, C. (eds.). Springer Verlag, p. 1-16 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9236).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    4 Citations (Scopus)
  • 2014

    CakeML: A verified implementation of ML

    Kumar, R., Myreen, M. O., Norrish, M. & Owens, S., 2014, POPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 179-191 13 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    211 Citations (Scopus)
  • 2013

    Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω1

    Norrish, M. & Huffman, B., 2013, Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. p. 133-146 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7998 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    7 Citations (Scopus)

  • Tableaux for verification of data-centric processes

    Bauer, A., Baumgartner, P., Diller, M. & Norrish, M., 2013, Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings. p. 28-43 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8123 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    1 Citation (Scopus)
  • 2012

    A string of pearls: Proofs of Fermat's Little Theorem

    Chan, H. L. & Norrish, M., 2012, Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings. p. 188-207 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7679 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    2 Citations (Scopus)
  • 2011

    Mechanised computability theory

    Norrish, M., 2011, Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings. p. 297-311 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6898 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    26 Citations (Scopus)
  • 2010

    (Nominal) unification by recursive descent with triangular substitutions

    Kumar, R. & Norrish, M., 2010, Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings. p. 51-66 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6172 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    15 Citations (Scopus)

  • A formalisation of the normal forms of context-free grammars in HOL4

    Barthwal, A. & Norrish, M., 2010, Computer Science Logic - 24th International Workshop, CSL 2010, and 19th Annual Conference of the EACSL, Proceedings. p. 95-109 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6247 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    5 Citations (Scopus)

  • Mechanisation of PDA and grammar equivalence for context-free languages

    Barthwal, A. & Norrish, M., 2010, Logic, Language, Information and Computation - 17th International Workshop, WoLLIC 2010, Proceedings. p. 125-135 11 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6188 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    5 Citations (Scopus)
  • 2009

    Mind the gap: A verification framework for low-level C

    Winwood, S., Klein, G., Sewell, T., Andronick, J., Cock, D. & Norrish, M., 2009, Theorem Proving in Higher Order Logics - 22nd International Conference, TPHOLs 2009, Proceedings. p. 500-515 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5674 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    33 Citations (Scopus)

  • SeL4: Formal verification of an OS kernel

    Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H. & Winwood, S., 2009, SOSP'09 - Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles. p. 207-220 14 p. (SOSP'09 - Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    1222 Citations (Scopus)

  • Verified, executable parsing

    Barthwal, A. & Norrish, M., 2009, Programming Languages and Systems - 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, Proceedings. p. 160-174 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5502).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access
    30 Citations (Scopus)
  • 2008

    A brief overview of HOL4

    Slind, K. & Norrish, M., 2008, Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Springer Verlag, p. 28-32 5 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5170 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    208 Citations (Scopus)
  • 2007

    Barendregt's variable convention in rule inductions

    Urban, C., Berghofer, S. & Norrish, M., 2007, Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. Springer Verlag, p. 35-50 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4603 LNAI).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    38 Citations (Scopus)

  • Proof pearl: De Bruijn terms really do work

    Norrish, M. & Vestergaard, R., 2007, Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings. Springer Verlag, p. 207-222 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4732 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    13 Citations (Scopus)

  • Types, bytes, and separation logic

    Tuch, H., Klein, G. & Norrish, M., 2007, Conference Record of POPL 2007: The 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Papers Presented at the Symposium. p. 97-108 12 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    59 Citations (Scopus)
  • 2006

    Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations

    Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M. & Wansbrough, K., 2006, Conference Record of POPL 2006: 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 55-66 12 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    16 Citations (Scopus)
  • 2005

    A formal treatment of the Barendregt variable convention in rule inductions

    Urban, C. & Norrish, M., 2005, MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding. Association for Computing Machinery, p. 25-32 8 p. (MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    13 Citations (Scopus)