Matthew Hague
|
Matthew
Hague
Wolfson Building, Parks Road, Oxford OX1 3QD |
Interests
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.
Biography
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.
Links
Some pictures
Yow -- a Zippy The Pinhead plugin for Vim
OCaml source code tagger -- plugin for GNU Global (gtags)
Talk slides for Edinburgh
Selected Publications
| A Saturation Method for the Modal Mu-Calculus over Pushdown Systems Matthew Hague and C.-H. Luke Ong 2010. Submitted to Information and Control, CONCUR special issue. |
| Extended Comuptation Tree Logic (Extended Abstract) Ronald Alexsson, Matthew Hague, Stephan Kreutzer, Martin Lange and Markus Latte 2010. Submitted |
| BOOM: Taking boolean program model checking one step further Gerard Basler et al. 2010. To appear in TACAS 2010 |
Info
|
Themes |
|
|
Activities |
Game Semantics and its Applications | Metacomputation | Hardware Verification | Model Checking |
|
Supervisor |