Log

Last updated 18/12/2024.

2025

In 2025 I will take up a position at the University of Southampton.

helping with Theorem Proving and Machine Learning in the age of LLMs: SoA and Future Perspectives

2024

talk Implementing the Expressive Power of Temporal Message Passing at the Stream Reasoning Workshop 2024
SAT solving for variants of first-order subsumption in Formal Methods in System Design
talk AVATAR: 10 years on at Dagstuhl seminar 24421: SAT and Interactions
substitute for Laura Kovács at the FM 2024 Doctoral Symposium
Forward Reasoning in Hindsight at AITP 2024
preprint Expressive Power of Temporal Message Passing
program committee for the Workshop on Composite AI
Reducibility Constraints in Superposition at IJCAR 2024
Rewriting and Inductive Reasoning and Scaling Game-Theoretic Security Reasoning at LPAR-25
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model at S&P 2024
reviewer for the Journal of Symbolic Computation
program committee for AITP 2024
delivering the formal methods MSc seminar
reviewer for the Artificial Intelligence Journal
preprint Spanning Matrices via Satisfiability Solving
lecturing at the SAT/SMT/AR summer school 2024
organiser for the 8^th Vampire workshop
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
committee for the VCLA International Student awards

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

In 2021 I took a position with Laura Kovács at TU Wien working on the ERC project ARTIST.

talk Learning From Subgoals at the formal methods workshop of Eszterházy Károly Catholic University
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 at Manchester 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

BA

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