Michael Norrish

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2022

Mechanizing Soundness of Off-Policy Evaluation.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Kalas: A Verified, End-To-End Compiler for a Choreographic Language.

[BibT_eX]

[DOI]

Johannes Åman Pohjola

Alejandro Gómez-Londoño

James Shaker

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021

TacticToe: Learning to Prove with Tactics.

[BibT_eX]

[DOI]

J. Autom. Reason., 2021

Mechanisation of the AKS Algorithm.

[BibT_eX]

[DOI]

J. Autom. Reason., 2021

TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning.

[BibT_eX]

[DOI]

Proceedings of the Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, 2021

Seed selection for successful fuzzing.

[BibT_eX]

[DOI]

Proceedings of the ISSTA '21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2021

On the formalisation of Kolmogorov complexity.

[BibT_eX]

[DOI]

Elliot Catt

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

Proof-Producing Synthesis of CakeML from Monadic HOL Functions.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Mechanised Modal Model Theory.

[BibT_eX]

[DOI]

Yiming Xu

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

The verified CakeML compiler backend.

[BibT_eX]

[DOI]

J. Funct. Program., 2019

Classification of Finite Fields with Applications.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Proof Pearl: Bounding Least Common Multiples with Triangles.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API.

[BibT_eX]

[DOI]

J. ACM, 2019

MoonLight: Effective Fuzzing with Near-Optimal Corpus Distillation.

[BibT_eX]

[DOI]

CoRR, 2019

Verified compilation on a verified processor.

[BibT_eX]

[DOI]

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Designing a low-level virtual machine for implementing real-time managed languages.

[BibT_eX]

[DOI]

Javad Ebrahimian Amiri

Stephen M. Blackburn

Antony L. Hosking

Proceedings of the 11th ACM SIGPLAN International Workshop on Virtual Machines and Intermediate Languages, 2019

A Verified Compositional Algorithm for AI Planning.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Modular synthesis of verified verifiers of computation with STV algorithms.

[BibT_eX]

[DOI]

Milad K. Ghale

Dirk Pattinson

Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, 2019

2018

Formally Verified Algorithms for Upper-Bounding State Space Diameters.

[BibT_eX]

[DOI]

J. Autom. Reason., 2018

Learning to Prove with Tactics.

[BibT_eX]

[DOI]

CoRR, 2018

Verified Certificate Checking for Counting Votes.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Hop, Skip, & Jump: Practical On-Stack Replacement for a Cross-Platform Language-Neutral VM.

[BibT_eX]

[DOI]

Proceedings of the 14th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments, 2018

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

[BibT_eX]

[DOI]

Simon Jantsch

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

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

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Verifying efficient function calls in CakeML.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2017

Verified Characteristic Formulae for CakeML.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2017

A State-Space Acyclicity Property for Exponentially Tighter Plan Length Bounds.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Seventh International Conference on Automated Planning and Scheduling, 2017

2016

Rust as a language for high performance GC implementation.

[BibT_eX]

[DOI]

Proceedings of the 2016 ACM SIGPLAN International Symposium on Memory Management, Santa Barbara, CA, USA, June 14, 2016

A new verified compiler backend for CakeML.

[BibT_eX]

[DOI]

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2015

Draining the Swamp: Micro Virtual Machines as Solid Foundation for Language Development.

[BibT_eX]

[DOI]

Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Stop and go: understanding yieldpoint behavior.

[BibT_eX]

[DOI]

Proceedings of the 2015 ACM SIGPLAN International Symposium on Memory Management, 2015

Mechanisation of AKS Algorithm: Part 1 - The Main Theorem.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Exploiting Symmetries by Planning for a Descriptive Quotient.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

2014

A mechanisation of some context-free language theory in HOL4.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2014

CakeML: a verified implementation of ML.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

An Approach for Proving the Correctness of Inspector/Executor Transformations.

[BibT_eX]

[DOI]

Michelle Mills Strout

Proceedings of the Languages and Compilers for Parallel Computing, 2014

Beagle as a HOL4 external ATP method.

[BibT_eX]

[DOI]

Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

2013

A String of Pearls: Proofs of Fermat's Little Theorem.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2013

Tableaux for Verification of Data-Centric Processes.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1.

[BibT_eX]

[DOI]

Brian Huffman

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax.

[BibT_eX]

[DOI]

James Cheney

René Vestergaard

J. Autom. Reason., 2012

Reasoning with Data-Centric Business Processes

[BibT_eX]

[DOI]

Andreas Klaus Bauer

Peter Baumgartner

CoRR, 2012

2011

Mechanised Computability Theory.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010

seL4: formal verification of an operating-system kernel.

[BibT_eX]

[DOI]

Commun. ACM, 2010

Mechanisation of PDA and Grammar Equivalence for Context-Free Languages.

[BibT_eX]

[DOI]

Proceedings of the Logic, 2010

(Nominal) Unification by Recursive Descent with Triangular Substitutions.

[BibT_eX]

[DOI]

Ramana Kumar

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A Formalisation of the Normal Forms of Context-Free Grammars in HOL4.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009

Rewriting Conversions Implemented with Continuations.

[BibT_eX]

[DOI]

J. Autom. Reason., 2009

Mind the Gap.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

seL4: formal verification of an OS kernel.

[BibT_eX]

[DOI]

Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

Verified, Executable Parsing.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2009

2008

A Brief Overview of HOL4.

[BibT_eX]

[DOI]

Konrad Slind

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service.

[BibT_eX]

[DOI]

Tom Ridge

Peter Sewell

Proceedings of the FM 2008: Formal Methods, 2008

2007

Proof Pearl: De Bruijn Terms Really Do Work.

[BibT_eX]

[DOI]

René Vestergaard

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

Types, bytes, and separation logic.

[BibT_eX]

[DOI]

Harvey Tuch

Gerwin Klein

Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Barendregt's Variable Convention in Rule Inductions.

[BibT_eX]

[DOI]

Christian Urban

Stefan Berghofer

Proceedings of the Automated Deduction, 2007

2006

Mechanising lambda-calculus using a classical first order theory of terms with permutations.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 2006

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

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

2005

Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.

[BibT_eX]

[DOI]

Konrad Slind

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGCOMM 2005 Conference on Applications, 2005

A formal treatment of the barendregt variable convention in rule inductions.

[BibT_eX]

[DOI]

Christian Urban

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2005

2004

Recursive Function Definition for Types with Binders.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

2003

The PROSPER toolkit.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2003

Complete Integer Decision Procedures as Derived Rules in HOL.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

Mechanising Hankin and Barendregt using the Gordon-Melham axioms.

[BibT_eX]

[DOI]

Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

2002

A Thread of HOL Development.

[BibT_eX]

[DOI]

Konrad Slind

Comput. J., 2002

Rigour is good for you <i>and</i> feasible: reflections on formal treatments of C and UDP sockets.

[BibT_eX]

[DOI]

Peter Sewell

Keith Wansbrough

Proceedings of the 10th ACM SIGOPS European Workshop, Saint-Emilion, France, July 1, 2002, 2002

Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2002

2000

The PROSPER Toolkit.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

1999

C formalised in HOL

[BibT_eX]

[DOI]

PhD thesis, 1999

Deterministic Expressions in C.

[BibT_eX]

[DOI]