I am interested in Games, Automata and Logics and their applications in verification and synthesis. I am currently writing my thesis on Saturation Methods for Global Model-Checking Pushdown Systems. This contains results for reachability over higher-order pushdown systems, Buchi games for order-2 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 also researching the the pushdown model-checker Moped and Java with Jimple, Bandera, abstraction and concurrency in mind.
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 am currently a DPhil student studying formal software verification under the supervison of Prof. Luke Ong. I am a student a St. John's College.
As an undergraduate I studied an MEng in Computing at Imperial College London.
I helped with the organisation of CSL 2005 and BCTCS 2007.
