My Journey to the Dark Side
- Speaker: Dr Giles Reger (University of Manchester)
- Host: Antoniu Pop
- 22nd March 2017 at 14:00 in Kilburn L.T 1.5
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 I will describe my journey from runtime verification (the not-so-dark side) to automated theorem proving (the dark side), and my 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 I have addressed in my research and will address 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. My research in this area has, therefore, been to explore heuristic methods for answering particular instances of this question. I will motivate and describe the problems and solutions in this space addressed by my research, and show how they have improved the Vampire theorem prover.