I am interested in Games, Automata and Logics and their applications in verification and synthesis. I am currently writing my thesis on Global Model-Checking of Higher-Order Pushdown Systems. This contains results for reachability, Buchi and parity games. 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, 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.
