## 2024

- preprint
*Reducibility Constraints in Superposition* - preprint
*Spanning Matrices via Satisfiability Solving* - lecturing at the SAT/SMT/AR summer school 2024
- program committee for PAAR 2024
- co-chair of IWIL 2024
- organiser for the Workshop on Alignment of Proof Systems and Machine Learning
- artefact evaluation co-chair for TACAS 2024

## 2023

*CheckMate: Automated Game-Theoretic Security Reasoning*at CCS 2023- talk
*Hands-On with Vampire*for the Knowledge Processing and Information Systems group at Potsdam *Embedding the Connection Calculus in Satisfiability Modulo Theories*at AReCCa 2023*Lemmas: Generation, Selection, Application*and*Non-Classical Logics in Satisfiability Modulo Theories*at TABLEAUX 2023*Learning to Identify Useful Lemmas from Failure*at AITP 2023- program committee for AReCCa 2023
- preprint
*CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model* *Superposition with Delayed Unification*and*SAT-based Subsumption Resolution*at CADE-29- entered Vampire into CASC-29
- program committee for SYNASC 2023
- invited talk
*Deploying Neural Models for Theorem Proving*at JEPNWPAMLTPDGD^{3} - co-chair of IWIL 2023
- organiser for the 7
^{th}Vampire workshop - program committee for AITP 2023
- program committee for TABLEAUX 2023
- committee for the VCLA International Student awards

## 2022

- preprint
*Linear Refutation and Clause Splitting* - delivered the formal methods MSc seminar
- invited talk
*Machine Learning for Theorem Proving: What I Wish I Had Known 5 Years Ago*at AITP 2022 *The Rapid Software Verification Framework*at FMCAD 2022*Automating Security Analysis of Off-Chain Protocols*at FMBC 2022*Reuse of Introduced Symbols in Automatic Theorem Provers*and*The Vampire Approach to Induction*at PAAR 2022- program committee for AITP 2022

## 2021

- talk
*Learning From Subgoals*at the formal methods workshop of Eszterházy Károly Catholic University **new position**at TU Wien, Austria with Laura Kovács, working on the ERC project ARTIST*On Evaluating Theorem Provers*at ARCADE 2021*A Multithreaded Vampire with Shared Persistent Grounding*at FMCAD 2021- program committee for PDAR 2021
- Eliminating Models during Model Elimination at TABLEAUX 2021

## 2020

In 2020 I took a position with Giles Reger working on the EPSRC project CAPS: Collaborative Architectures for Proof Search.## PhD

From 2017 to 2020 I was a PhD student in the school of Computer Science, University of Manchester. My thesis was on*Applications of Machine Learning to Automated Reasoning*, supervised by Giles Reger and Andrei Voronkov. You might be looking for material from that time, which includes

*lazyCoP: Lazy Paramodulation meets Neurally-Guided Search**Reinforced External Guidance for Theorem Provers**Directed Graph Networks for Logical Reasoning**Old or Heavy? Decaying Gracefully with Age/Weight Shapes**A Neurally-Guided, Parallel Theorem Prover**Dynamic Strategy Power: Empower the strong and abandon the weak*

## BA

Before*that*, I read Computer Science (with Physics!) at the Computer Laboratory, University of Cambridge. My Part II dissertation was entitled Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed λ-Calculus, supervised by Dominic Mulligan and Victor Gomes. It has a corresponding entry in the Archive of Formal Proofs.