Matthew Hague
- Matthew Hague
- Professor
- Bedford 2-08
- Department of Computer Science
- Royal Holloway University of London
- Egham Hill, Egham, TW20 0EX
- E-Mail: matthew hague * rhul ac uk (where *=@ and spaces are .)
Journal Publications
Collapsible Pushdown Parity Games
In ACM Transactions of Computational Logic (ToCL), 2021
CSS Minification via Constraint Solving
In ACM Transactions on Programming Languages and Systems (TOPLAS), 2019.
Decidable models of integer-manipulating programs with recursive parallelism
In Theoretical Computer Science, Reachability Problems 2016 Special Issue, 2018
Collapsible Pushdown Automata and Recursion Schemes
In Transactions on Computational Logic, Volume 18, 2017
A Saturation Method for the Modal Mu‐Calculus over Pushdown Systems
In Information and Computation, 2010.
CONCUR special issue.
Symbolic Backwards‐Reachability Analysis for
Higher‐Order Pushdown Systems
In Logical Methods in Computer Science (LMCS), Vol. 4, 2008.
FoSSaCS 2007, special issue.
Conference Publications
Parikh's Theorem Made Symbolic
In Principles of Programming Languages (POPL), 2024.
Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables
To appear in the Principles of Programming Languages (POPL), 2022.
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
To appear in the International Symposium of Automated Technology for Verification and Analysis (ATVA), 2020.
Monadic Decomposition in Integer Linear Arithmetic
In the International Joint Conference on Automated Reasoning (IJCAR), 2020.
Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations
In Principles of Programming Languages (POPL), 2019.
Constrained Dynamic Tree Networks
To appear in Reachability Problems, 2018.
Optimal Strategies in Pushdown Reachability Games
To appear in Mathematical Foundations of Computer Science, 2018.
Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems
To appear in Mathematical Foundations of Computer Science, 2018.
What Is Decidable about String Constraints with the ReplaceAll Function
In Principles of Programming Languages (POPL), 2018.
Domains for Higher-Order Games
In Mathematical Foundations of Computer Science (MFCS), 2017.
Decidable models of integer-manipulating programs with recursive parallelism
To appear in Reachability Problems (RP), 2016.
Generating Concurrency Checks Automatically
In Formal Techniques for Java-Like Programs (FTfJP), 2016.
Unboundedness and Downward Closures of Higher-Order Pushdown Automata
In POPL, 2016.
Detecting Redundant CSS Rules in HTML5 Applications: A Tree Rewriting Approach
To appear in OOPSLA, 2015.
Conference Version (pdf) |
Full Version (pdf) |
arXiv:1412.5143 [cs.LO] |
Submitted TreePed (tgz) |
TreePed (bitbucket)
Regular Strategies in Pushdown Reachability Games
In Reachability Problems (RP), 2014.
Senescent Ground Tree Rewrite Systems
In Computer Science Logic -- Logic in Computer Science (CSL-LICS), 2014.
Saturation Algorithms for Model-Checking Pushdown Systems
Invited survey for the International Conference on Automata and Formal Languages (AFL), 2014.
Saturation of Concurrent Collapsible Pushdown Systems
In Foundations of Software Technology and Theoretical
Computer Science (FSTTCS), 2013.
C-SHORe: A Collapsible Approach to Higher-Order Verification
In the International Conference on Functional Programming (ICFP), 2013.
A Saturation Method for Collapsible Pushdown Systems
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
In Computer Aided Verification (CAV), 2012.
Parameterised Pushdown Systems with Non‐Atomic Writes
In Foundations of Software Technology and Theoretical
Computer Science (FSTTCS), 2011.
Model Checking Recursive Programs with Numeric Data Types
In Computer Aided Verification (CAV), 2011.
The Complexity of Model Checking (Collapsible) Higher‐Order Pushdown Systems
In Foundations of Software Technology and Theoretical
Computer Science (FSTTCS), 2010.
Analysing Mu‐Calculus Properties of Pushdown Systems (Tool Presentation)
In SPIN, 2010.
Extended Computation Tree Logic (Extended Abstract)
In the International Conference on Logic for Programming
Artificial Intelligence and Reasoning (LPAR), 2010.
BOOM: Taking boolean program model checking one step further
In Tools and Algorithms for the Construction and Analysis of
Systems (TACAS), 2010.
Winning Regions of Pushdown Parity Games: A Saturation Method
In the International Conference on Concurrency Theory (CONCUR), 2009.
Winning Regions of Higher‐Order Pushdown Games
In Logic in Computer Science (LICS), 2008.
Collapsible Pushdown Automata and Recursion Schemes
In Logic in Computer Science (LICS), 2008.
Symbolic Backwards Reachability Analysis for Higher‐Order Pushdown Systems
In Foundations of Software Science and Computation
Structures (FoSSaCS), 2007.
From Separation Logic to First‐Order Logic
In Foundations of Software Science and Computation
Structures (FoSSaCS), 2005.
Theses
Saturation Methods for Global Model‐Checking Pushdown Systems
PhD Thesis, Oxford University, 2009.
Submitted Jan 2009, minor corrections May 2009,
Clarification on page 164, Dec 2009. Error noted in Section
6.1, Jan 2011 (Corrected in FSTTCS 2010).
Static Checkers for Tree Structures and Heaps
Master's Thesis, Imperial College London, 2004.
General Nonsense
PGP Public Key:
my PGP public key, should you ever want to send me anything sensitive.
(Fingerprint: 538C C71A 48BA F957 C3EB A156 0F23 777D B1C9 1B45.)
(Fingerprint: 538C C71A 48BA F957 C3EB A156 0F23 777D B1C9 1B45.)
F-Droid (a thing i like): a calm, open-sourced alternative to
hassleful Android app markets (and apps).
