• My Journey to the Dark Side by Dr Giles Reger 22/03/17 KB L.T. 1.5 14:00

    Published: Friday, 10 March 2017

    My Journey to the Dark Side by Dr Giles Reger 22/03/17 KB L.T. 1.5 14:00

    My Journey to the Dark Side by Dr Giles Reger 22/03/17 KB L.T. 1.5 14:00

    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.

     

    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 here 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.

    gravatar Karon Mee
Generated: Sunday, 30 April 2017 10:07:28
Last change: Friday, 10 March 2017 14:31:57
▲ Up to the top