Matthew Hague

Matthew Hague

Former Member

Leaving date: 1st September 2011

Themes:

• Quantum
• Automated Verification

Completed Projects:

• Metacomputation

Interests

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.

Biography

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 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.

See also

• Some pictures
• Yow -- a Zippy The Pinhead plugin for Vim

Selected Publications

View AllManage publications

• Synchronisation− and Reversal−Bounded Analysis of Multithreaded Programs with Counters

  Matthew Hague and Anthony Widjaja Lin

  In Computer Aided Verification (CAV), 2012.

  Details about Synchronisation− and Reversal−Bounded Analysis of Multithreaded Programs with Counters | BibTeX data for Synchronisation− and Reversal−Bounded Analysis of Multithreaded Programs with Counters | Download  (pdf) of Synchronisation− and Reversal−Bounded Analysis of Multithreaded Programs with Counters

• Parameterised Pushdown Systems with Non−Atomic Writes

  M. Hague

  In FSTTCS. 2011.

  To appear.

  Details about Parameterised Pushdown Systems with Non−Atomic Writes | BibTeX data for Parameterised Pushdown Systems with Non−Atomic Writes | Download  (pdf) of 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.

  Prototypical implementation: [tgz] [txz].

  Details about Model Checking Recursive Programs with Numeric Data Types | BibTeX data for Model Checking Recursive Programs with Numeric Data Types | Download  (pdf) of Model Checking Recursive Programs with Numeric Data Types

Activities

• RECOUNT
• Hardware Verification
• Model Checking