I am interested in Games, Automata and Logics and their applications in verification and synthesis. I recently completed my thesis on Saturation Methods for Global Model-Checking Pushdown Systems. This contains results for reachability/model-checking over higher-order pushdown systems and parity games for order-1 pushdown systems. I have also worked with William Blum on a SAT-based LTL model checker which uses Linear Weak Alternating Automata.
I am currently continuing research into pushdown systems and MSO and studying Vector Addition Systems/Petri-Nets.
As an undergraduate my key interests were logics, and my final year project was an implementation of a decision procedure for the Static Ambient Logic and a related translation between Separation Logic and First Order Logic. My project supervisor was Dr. Philippa Gardner.
I recently completed my DPhil studying formal software verification under the supervison of Prof. Luke Ong and was a student a St. John's College. I am currently employed as a research assistant.
As an undergraduate I studied an MEng in Computing at Imperial College London.
I helped with the organisation of CSL 2005 and BCTCS 2007.
