My Journey to the Dark Side by Dr. Giles Reger

Time: 14:00 - 16:00

Venue: Lecture Theatre 1.5, The Kilburn Building,

Sorry, this event has now ended.

"In 2013 I was presented with a choice: a postdoc in an area related to my PhD work, or to join the Dark Side of theorem proving. I chose the Dark Side."

In this talk Dr Giles Reger will describe his journey from runtime verification (the not-so-dark side) to automated theorem proving (the dark side), and his ongoing research in both fields. Runtime verification (RV) is the problem of checking whether a single execution of a program (or more generally, a system) conforms to a formally given specification of correct behaviour. This requires notions of what an execution of a program looks like, what a formal specification looks like, and how to do the checking efficiently, these are the questions that will be addressed in this talk. Automated Theorem Proving (ATP) is the job of taking a problem written in formal logic and asking the question ‘is this true’? Here the notions of what logic is and what truth means are well-defined, but the question is undecidable for first-order logic, our logic of choice. Dr Reger's research in this area has been to explore heuristic methods for answering particular instances of this question. He will motivate and describe the problems and solutions in this space addressed by his research, and show how they have improved the Vampire theorem prover.

Dr Giles Reger joined the Formal Methods group as a Lecturer in Febuary 2016. He was previously a member of the group as a PhD student and research associate. His current reasearch interests include automated reasoning and dynamic program analysis, both with a focus on software verification. Since 2014 he has been a main contributor to the world-leading Vampire theorem prover project based in Manchester, and has contributed to the recent successes at the CASC and SMTCOMP competitions. Core to this success was the integration of Vampire with the Z3 SMT solver developed by  Microsoft Research. In the area of dynamic program analysis, also known as runtime verification, he leads an international working group (via an EU-funded COST project) aiming to standardise languages and methods for dynamic program properties. He is also the lead developer of the MarQ runtime verification tool, which has won medals in the last three runtime verification competitions, which he now co-organises. This work includes on ongoing collaboration with NASA's Jet Propulsion Laboratory.