| 2025 |
| Game Modeling of Blockchain Protocols | iFM 2025 |
| Divide and Conquer: a Compositional Approach to Game-Theoretic Security | OOPSLA 2025 |
| Constraint Learning for Non-Confluent Proof Search | TABLEAUX 2025 |
| Finding Connections via Satisfiability Solving | TABLEAUX 2025 |
| First-Order Equational Reasoning via E-graphs and λ-terms | AITP 2025 |
| Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories | CADE-30 |
| The Vampire Diary | CAV 2025 (distinguished!) |
| Expressive Power of Temporal Message Passing | AAAI 2025 |
| Case Study: Verified Vampire Proofs in the λΠ-calculus Modulo | preprint |
| 2024 |
| SAT solving for variants of first-order subsumption | FMSD |
| Forward Reasoning in Hindsight | AITP 2024 |
| Reducibility Constraints in Superposition | IJCAR 2024 |
| Rewriting and Inductive Reasoning | LPAR-25 |
| Scaling Game-Theoretic Security Reasoning | LPAR-25 |
| CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model | S&P 2024 |
| 2023 |
| CheckMate: Automated Game-Theoretic Security Reasoning | CCS 2023 |
| Embedding the Connection Calculus in Satisfiability Modulo Theories | AReCCa 2023 |
| Lemmas: Generation, Selection, Application | TABLEAUX 2023 |
| Non-Classical Logics in Satisfiability Modulo Theories | TABLEAUX 2023 |
| Learning to Identify Useful Lemmas from Failure | AITP 2023 |
| Superposition with Delayed Unification | CADE-29 |
| SAT-based Subsumption Resolution | CADE-29 |
| 2022 |
| Linear Refutation and Clause Splitting | preprint |
| The Rapid Software Verification Framework | FMCAD 2022 |
| Automating Security Analysis of Off-Chain Protocols | FMBC 2022 |
| Reuse of Introduced Symbols in Automatic Theorem Provers | PAAR 2022 |
| The Vampire Approach to Induction | PAAR 2022 |
| 2021 |
| On Evaluating Theorem Provers | ARCADE 2021 |
| A Multithreaded Vampire with Shared Persistent Grounding | FMCAD 2021 |
| Eliminating Models during Model Elimination | TABLEAUX 2021 |
| lazyCoP: Lazy Paramodulation meets Neurally-Guided Search | TABLEAUX 2021 |
| 2020 |
| Reinforced External Guidance for Theorem Provers | PAAR 2020 |
| Directed Graph Networks for Logical Reasoning | PAAR 2020 |
| 2019 |
| Old or Heavy? Decaying Gracefully with Age/Weight Shapes | CADE-27 |
| A Neurally-Guided, Parallel Theorem Prover | FroCoS 2019 |
| 2018 |
| Dynamic Strategy Priority: Empower the strong and abandon the weak | PAAR 2018 |