Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors. - Howard Barringer; Yliès Falcone; Klaus Havelund; Giles Reger; David E. Rydeheard (FM, 2012)

A pattern-based approach to parametric specification mining. - Giles Reger; Howard Barringer; David E. Rydeheard (ASE, 2013)

A Tutorial on Runtime Verification. - Yliès Falcone; Klaus Havelund; Giles Reger (Engineering Dependable Software Systems, 2013)

The Challenges of Evaluating a New Feature in Vampire. - Giles Reger; Martin Suda 001; Andrei Voronkov (Vampire Workshop, 2014)

Automata based monitoring and mining of execution traces. - Giles Reger (2014)

The Uses of SAT Solvers in Vampire. - Giles Reger; Martin Suda 001 (Vampire Workshop, 2015)

Playing with AVATAR. - Giles Reger; Martin Suda 001; Andrei Voronkov (CADE, 2015)

Cooperating Proof Attempts. - Giles Reger; Dmitry Tishkovsky; Andrei Voronkov (CADE, 2015)

Second International Competition on Runtime Verification CRV 2015. - Yliès Falcone; Dejan Nickovic; Giles Reger; Daniel Thoma (RV, 2015)

Suggesting Edits to Explain Failing Traces. - Giles Reger (RV, 2015)

From First-order Temporal Logic to Parametric Trace Slicing. - Giles Reger; David E. Rydeheard (RV, 2015)

Specification of Parametric Monitors. - Klaus Havelund; Giles Reger (SyDe Summer School, 2015)

MarQ: Monitoring at Runtime with QEA. - Giles Reger; Helena Cuenca Cruz; David E. Rydeheard (TACAS, 2015)

Automata-based Pattern Mining from Imperfect Traces. - Giles Reger; Howard Barringer; David E. Rydeheard (ACM SIGSOFT Softw. Eng. Notes, 2015)

Selecting the Selection. - Krystof Hoder; Giles Reger; Martin Suda 001; Andrei Voronkov (IJCAR, 2016)

Global Subsumption Revisited (Briefly). - Giles Reger; Martin Suda 001 (Vampire@IJCAR, 2016)

Better Proof Output for Vampire. - Giles Reger (Vampire@IJCAR, 2016)

The vampire and the FOOL. - Evgenii Kotelnikov; Laura Kovács; Giles Reger; Andrei Voronkov (CPP, 2016)

New Techniques in Clausal Form Generation. - Giles Reger; Martin Suda 001; Andrei Voronkov (GCAI, 2016)

AVATAR Modulo Theories. - Giles Reger; Nikolaj S. Bjørner; Martin Suda 001; Andrei Voronkov (GCAI, 2016)

Considering Typestate Verification for Quantified Event Automata. - Giles Reger (ISoLA (1), 2016)

What Is a Trace? A Runtime Verification Perspective. - Giles Reger; Klaus Havelund (ISoLA (2), 2016)

An Overview of MarQ. - Giles Reger (RV, 2016)

Third International Competition on Runtime Verification - CRV 2016. - Giles Reger; Sylvain Hallé; Yliès Falcone (RV, 2016)

Finding Finite Models in Multi-sorted First-Order Logic. - Giles Reger; Martin Suda 001; Andrei Voronkov (SAT, 2016)

Runtime Verification Logics A Language Design Perspective. - Klaus Havelund; Giles Reger (Models, Algorithms, Logics and Tools, 2017)

Checkable Proofs for First-Order Theorem Proving. - Giles Reger; Martin Suda 001 (ARCADE@CADE, 2017)

A Report of ARCADE 2017. - Giles Reger; Dmitriy Traytel (ARCADE@CADE, 2017)

Set of Support for Theory Reasoning. - Giles Reger; Martin Suda 001 (IWIL@LPAR, 2017)

A Report of RV-CuBES 2017. - Giles Reger (RV-CuBES, 2017)

Instantiation and Pretending to be an SMT Solver with Vampire. - Giles Reger; Martin Suda 001; Andrei Voronkov (SMT, 2017)

Testing a Saturation-Based Theorem Prover: Experiences and Challenges. - Giles Reger; Martin Suda 001; Andrei Voronkov (TAP@STAF, 2017)

Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version). - Giles Reger; Martin Suda 001; Andrei Voronkov (CoRR, 2017)

A Story of Parametric Trace Slicing, Garbage and Static Analysis. - Giles Reger (PrePost@iFM, 2017)

A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462). - Klaus Havelund; Martin Leucker; Giles Reger; Volker Stolz (Dagstuhl Reports, 2017)

Set of Support for Higher-Order Reasoning. - Ahmed Bhayat; Giles Reger (PAAR@FLoC, 2018)

Dynamic Strategy Priority: Empower the Strong and Abandon the Weak. - Michael Rawson 001; Giles Reger (PAAR@FLoC, 2018)

Some Thoughts About FOL-Translations in Vampire. - Giles Reger (ARQNL@IJCAR, 2018)

A Broader View on Verification: From Static to Runtime and Back (Track Summary). - Wolfgang Ahrendt; Marieke Huisman; Giles Reger; Kristin Yvonne Rozier (ISoLA (2), 2018)

COST Action IC1402 Runtime Verification Beyond Monitoring. - Christian Colombo 001; Yliès Falcone; Martin Leucker; Giles Reger; César Sánchez 001; Gerardo Schneider; Volker Stolz (RV, 2018)

Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. - Giles Reger; Martin Suda 001; Andrei Voronkov (TACAS (1), 2018)

Specification of State and Time Constraints for Runtime Verification of Functions. - Joshua Heneage Dawes; Giles Reger (CoRR, 2018)

Introduction to Runtime Verification. - Ezio Bartocci; Yliès Falcone; Adrian Francalanza; Giles Reger (Lectures on Runtime Verification, 2018)

Monitoring Events that Carry Data. - Klaus Havelund; Giles Reger; Daniel Thoma; Eugen Zalinescu (Lectures on Runtime Verification, 2018)

Restricted Combinatory Unification. - Ahmed Bhayat; Giles Reger (CADE, 2019)

Old or Heavy? Decaying Gracefully with Age/Weight Shapes. - Michael Rawson 001; Giles Reger (CADE, 2019)

Induction in Saturation-Based Proof Search. - Giles Reger; Andrei Voronkov (CADE, 2019)

A Neurally-Guided, Parallel Theorem Prover. - Michael Rawson 001; Giles Reger (FroCos, 2019)

Symmetry Avoidance in MACE-Style Finite Model Finding. - Giles Reger; Martin Riener; Martin Suda 001 (FroCos, 2019)

Explaining Violations of Properties in Control-Flow Temporal Logic. - Joshua Heneage Dawes; Giles Reger (RV, 2019)

Specification of temporal properties of functions for runtime verification. - Joshua Heneage Dawes; Giles Reger (SAC, 2019)

International Competition on Runtime Verification (CRV). - Ezio Bartocci; Yliès Falcone; Giles Reger (TACAS (3), 2019)

VyPR2: A Framework for Runtime Verification of Python Web Services. - Joshua Heneage Dawes; Giles Reger; Giovanni Franzoni; Andreas Pfeiffer; Giacomo Govi (TACAS (2), 2019)

Boldly Going Where No Prover Has Gone Before. - Giles Reger (ARCADE@CADE, 2019)

The SMT Competition 2015-2018. - Tjark Weber; Sylvain Conchon; David Déharbe; Matthias Heizmann; Aina Niemetz; Giles Reger (J. Satisf. Boolean Model. Comput., 2019)

First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014. - Ezio Bartocci; Yliès Falcone; Borzoo Bonakdarpour; Christian Colombo 001; Normann Decker; Klaus Havelund; Yogi Joshi; Felix Klaedtke; Reed Milewicz; Giles Reger; Grigore Rosu; Julien Signoles; et al. (Int. J. Softw. Tools Technol. Transf., 2019)

Runtime Verification Past Experiences and Future Projections. - Klaus Havelund; Giles Reger; Grigore Rosu (Computing and Software Science, 2019)

A Knuth-Bendix-Like Ordering for Orienting Combinator Equations. - Ahmed Bhayat; Giles Reger (IJCAR (1), 2020)

A Combinator-Based Superposition Calculus for Higher-Order Logic. - Ahmed Bhayat; Giles Reger (IJCAR (1), 2020)

A Polymorphic Vampire - (Short Paper). - Ahmed Bhayat; Giles Reger (IJCAR (2), 2020)

Directed Graph Networks for Logical Reasoning (Extended Abstract). - Michael Rawson 001; Giles Reger (PAAR+SC²@IJCAR, 2020)

Pattern Extraction for Behaviours of Multi-Stage Threats via Unsupervised Learning. - Ahmed Abdulrahman Alghamdi; Giles Reger (CyberSA, 2020)

PerfCI: A Toolchain for Automated Performance Testing during Continuous Integration of Python Projects. - Omar Javed; Joshua Heneage Dawes; Marta Han; Giovanni Franzoni; Andreas Pfeiffer; Giles Reger; Walter Binder (ASE, 2020)

Analysing the Performance of Python-Based Web Services with the VyPR Framework. - Joshua Heneage Dawes; Marta Han; Omar Javed; Giles Reger; Giovanni Franzoni; Andreas Pfeiffer (RV, 2020)

On Evaluating Theorem Provers. - Michael Rawson 001; Giles Reger (ARCADE@CADE, 2021)

A Multithreaded Vampire with Shared Persistent Grounding. - Michael Rawson 001; Giles Reger (FMCAD, 2021)

lazyCoP: Lazy Paramodulation Meets Neurally Guided Search. - Michael Rawson 001; Giles Reger (TABLEAUX, 2021)

Eliminating Models During Model Elimination. - Michael Rawson 001; Giles Reger (TABLEAUX, 2021)

Making Theory Reasoning Simpler. - Giles Reger; Johannes Schoisswohl; Andrei Voronkov (TACAS (2), 2021)

A taxonomy for classifying runtime verification tools. - Yliès Falcone; Srdan Krstic; Giles Reger; Dmitriy Traytel (Int. J. Softw. Tools Technol. Transf., 2021)

From parametric trace slicing to rule systems. - Giles Reger; David E. Rydeheard (Int. J. Softw. Tools Technol. Transf., 2021)

To test, or not to test: A proactive approach for deciding complete performance test initiation. - Omar Javed; Prashant Singh; Giles Reger; Salman Toor (IEEE Big Data, 2022)

Getting Saturated with Induction. - Márton Hajdú; Petra Hozzová; Laura Kovács; Giles Reger; Andrei Voronkov (Principles of Systems Design, 2022)

The Rapid Software Verification Framework. - Pamina Georgiou; Bernhard Gleiss; Ahmed Bhayat; Michael Rawson 001; Laura Kovács; Giles Reger (FMCAD, 2022)

ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC. - Franz Brauße; Fedor Shmarov; Rafael Menezes; Mikhail R. Gadelha; Konstantin Korovin; Giles Reger; Lucas C. Cordeiro (ISSTA, 2022)

Lemmaless Induction in Trace Logic. - Ahmed Bhayat; Pamina Georgiou; Clemens Eisenhofer; Laura Kovács; Giles Reger (CICM, 2022)

Reuse of Introduced Symbols in Automatic Theorem Provers (short paper). - Michael Rawson 001; Martin Suda 001; Petra Hozzová; Giles Reger (PAAR@IJCAR, 2022)

Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities. - Kaled M. Alshmrany; Ahmed Bhayat; Franz Brauße; Lucas C. Cordeiro; Konstantin Korovin; Tom Melham; Mustafa A. Mustafa; Pierre Olivier; Giles Reger; Fedor Shmarov (SecDev, 2022)

Principles of Contract Languages (Dagstuhl Seminar 22451). - Dilian Gurov; Reiner Hähnle; Marieke Huisman; Giles Reger; Christian Lidström (Dagstuhl Reports, 2022)

A Toolkit for Automated Testing of Dafny. - Aleksandr Fedchin; Tyler Dean; Jeffrey S. Foster; Eric Mercer; Zvonimir Rakamaric; Giles Reger; Neha Rungta; Robin Salkeld; Lucas G. Wagner; Cassidy Waldrip (NFM, 2023)

ALASCA: Reasoning in Quantified Linear Arithmetic. - Konstantin Korovin; Laura Kovács; Giles Reger; Johannes Schoisswohl; Andrei Voronkov (TACAS (1), 2023)

LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling. - Muhammad A. A. Pirzada; Giles Reger; Ahmed Bhayat; Lucas C. Cordeiro (ASE, 2024)

The Vampire Diary. - Filip Bártek; Ahmed Bhayat; Robin Coutelier; Márton Hajdú; Matthias Hetzenberger; Petra Hozzová; Laura Kovács; Jakob Rath; Michael Rawson 001; Giles Reger; Martin Suda 001; Johannes Schoisswohl; et al. (CAV (3), 2025)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)