• Matthew Hague
  • Post-doctoral Researcher
  • Laboratoire d'Informatique Gaspard-Monge
  • Université Paris-Est
  • matthew hague * univ-mlv fr (where *=@ and spaces are .)

And now...

...i am here.


I am working on C-SHORe, a verification tool for higher-order recursion schemes with C. Broadbent, A. Carayol and O. Serre.

I am on the organising committee of DLT 2013.

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.


I completed my DPhil studying formal software verification under the supervison of Prof. Luke Ong and was a student a St. John's College. I was employed as a research assistant at the Oxford University, Department of Computing until 2011. Currently I am employed at IGM, Université Paris-Est under the supervision of Dr. Arnaud Carayol.

As an undergraduate I studied an MEng in Computing at Imperial College London.

I helped with the organisation of CSL 2005 and BCTCS 2007.

Recent Publications [View All] [dblp]

C-SHORe: A Collapsible Approach to Higher-Order Verification
C. Broadbent, A. Carayol, M. Hague and O. Serre
Submitted to Computer Aided Verification (CAV), 2013.
A Saturation Method for Collapsible Pushdown Systems
C. Broadbent, A. Carayol, M. Hague, and O. Serre
In the International Colloquium on Automata, Languages and Programming (ICALP), 2012.
Also in the Algorithms on Infinite State Systems (AISS) workshop, 2012.
Synchronisation‐ and Reversal‐Bounded Analysis of Multithreaded Programs with Counters
M. Hague and A. W. Lin
In Computer Aided Verification (CAV), 2012.

General Nonsense