Giles Reger

Giles Reger is a Senior Lecturer in the School of Computer Science at the University of Manchester, where he leads research in the Formal Methods Group. His academic background includes a BA in Computer Science from the University of Cambridge (2009), an MSc in Advanced Computer Science from the University of Manchester (2010, Highest Achiever Award), and a PhD from Manchester (2014) on Automata-based monitoring and mining of execution traces.

Research interests focus on:

• Theorem Proving: Core developer of the Vampire first-order ATP system, working on performance extensions and collaborative proving techniques
• Runtime Verification: Creator of the MarQ monitoring tool and organizer of the International Runtime Verification Competition
• Formal Methods: Applications in program verification, specification mining, and temporal logic

Publications emphasize automated reasoning, verification tools, and temporal specification languages, with recent work exploring neural-guided theorem proving and higher-order unification. His group consistently publishes at top venues like CADE, TACAS, and RV.

Awards include:

• Multiple division wins in SMTCOMP/CASC theorem proving competitions (2016-2020)
• FLoC Olympic Games medals for Vampire contributions (2018)

Advises PhD students including Michael Rawson (neural-guided proving) and Joshua Dawes (runtime verification). Leads the £1.3M EPSRC-funded SCorCH project (Secure Code for Capability Hardware) with Oxford/ARM/AWS. Coordinates the COST Action on Runtime Verification Beyond Monitoring.