Matthew Hague * cs ox ac uk (with * = @ and spaces are .)
Wolfson Building, Parks Road, Oxford OX1 3QD
... je suis ici.
I am responsible for the PDSolver tool.
I am interested in Games, Automata and Logics and their applications in verification and synthesis. I completed my thesis in 2009 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 am currently continuing theoretical and practical research into pushdown systems, implementations of model checking tools, and various other aspects of infinite state systems.
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 Prof. Philippa Gardner.
As an undergraduate I studied an MEng in Computing at Imperial College London.
Yow -- a Zippy The Pinhead plugin for Vim
OCaml source code tagger -- plugin for GNU Global (gtags)
Pulse-ctrl: a script implementing some useful command line Pulse Audio manipulations
Mutt-Display-Filter: for filtering long to: and cc: lists in Mutt
Mp3Imager: a rough and ready script for automatically downloading and embedding album art in mp3s
Parameterised Pushdown Systems with Non−Atomic Writes
Model Checking Recursive Programs with Numeric Data Types
Matthew Hague and Anthony Widjaja Lin
In Computer Aided Verification (CAV). 2011.
A Saturation Method for the Modal Mu−Calculus over Pushdown Systems
M. Hague and C.−H. L. Ong
In Information and Computation. 2010.
CONCUR special issue.