arXiv subjects

Matthew Hague

Publications and source records attributed to Matthew Hague.

At least 19 recordsLinked to original sources

arXiv2026

Synthesis and Verification of Transformer Programs (Technical Report)

C-RASP is a simple programming language that was recently shown to capture concepts expressible by transformers. In this paper, we develop new algorithmic techniques for automatically verifying C-RASPs. To this end, we establish a connection to the verification of synchronous dataflow programs in Lustre, which enables us to exploit state-of-the-art model checkers utilizing highly optimized SMT-solvers. Our second contribution addresses learning a C-RASP program in the first place. To this end, we provide a new algorithm for learning a C-RASP from examples using local search. We demonstrate efficacy of our implementation for benchmarks of C-RASPs in the literature, in particular in connection to the following applications: (1) transformer program optimization, and (2) constrained learning of transformer programs (based on a partial specification).

cs.LG↗

arXiv2025

General Decidability Results for Systems with Continuous Counters

Counters that hold natural numbers are ubiquitous in modeling and verifying software systems; for example, they model dynamic creation and use of resources in concurrent programs. Unfortunately, such discrete counters often lead to extremely high complexity. Continuous counters are an efficient over-approximation of discrete counters. They are obtained by relaxing the original counters to hold values over the non-negative rational numbers. This work shows that continuous counters are extraordinarily well-behaved in terms of decidability. Our main result is that, despite continuous counters being infinite-state, the language of sequences of counter instructions that can arrive in a given target configuration, is regular. Moreover, a finite automaton for this language can be computed effectively. This implies that a wide variety of transition systems can be equipped with continuous counters, while maintaining decidability of reachability properties. Examples include higher-order recursion schemes, well-structured transition systems, and decidable extensions of discrete counter systems. We also prove a non-elementary lower bound for the size of the resulting finite automaton.

cs.FL↗

arXiv2025

The Power of Regular Constraint Propagation (Technical Report)

The past decade has witnessed substantial developments in string solving. Motivated by the complexity of string solving strategies adopted in existing string solvers, we investigate a simple and generic method for solving string constraints: regular constraint propagation. The method repeatedly computes pre- or post-images of regular languages under the string functions present in a string formula, inferring more and more knowledge about the possible values of string variables, until either a conflict is found or satisfiability of the string formula can be concluded. Such a propagation strategy is applicable to string constraints with multiple operations like concatenation, replace, and almost all flavors of string transductions. We demonstrate the generality and effectiveness of this method theoretically and experimentally. On the theoretical side, we show that RCP is sound and complete for a large fragment of string constraints, subsuming both straight-line and chain-free constraints, two of the most expressive decidable fragments for which some modern string solvers provide formal completeness guarantees. On the practical side, we implement regular constraint propagation within the open-source string solver OSTRICH. Our experimental evaluation shows that this addition significantly improves OSTRICH's performance and makes it competitive with existing solvers. In fact, it substantially outperforms other solvers on random PCP and bioinformatics benchmarks. The results also suggest that incorporating regular constraint propagation alongside other techniques could lead to substantial performance gains for existing solvers.

cs.LO↗

arXiv2025

OSTRICH2: Solver for Complex String Constraints

We present OSTRICH2, the latest evolution of the SMT solver OSTRICH for string constraints. OSTRICH2 supports a wide range of complex functions on strings and provides completeness guarantees for a substantial fragment of string constraints, including the straight-line fragment and the chain-free fragment. OSTRICH2 provides full support for the SMT-LIB theory of Unicode strings, extending the standard with several unique features not found in other solvers: among others, parsing of ECMAScript regular expressions (including look-around assertions and capture groups) and handling of user-defined string transducers. We empirically demonstrate that OSTRICH2 is competitive to other string solvers on SMT-COMP benchmarks.

cs.LO↗

arXiv2023

Parikh's Theorem Made Symbolic

Parikh's Theorem is a fundamental result in automata theory with numerous applications in computer science: software verification (e.g. infinite-state verification, string constraints, and theory of arrays), verification of cryptographic protocols (e.g. using Horn clauses modulo equational theories) and database querying (e.g. evaluating path-queries in graph databases). Parikh's Theorem states that the letter-counting abstraction of a language recognized by finite automata or context-free grammars is definable in Presburger Arithmetic. Unfortunately, real-world applications typically require large alphabets - which are well-known to be not amenable to explicit treatment of the alphabets. Symbolic automata have proven in the last decade to be an effective algorithmic framework for handling large finite or even infinite alphabets. A symbolic automaton employs an effective boolean algebra, which offers a symbolic representation of character sets and often lends itself to an exponentially more succinct representation of a language. Instead of letter-counting, Parikh's Theorem for symbolic automata amounts to counting the number of times different predicates are satisfied by an input sequence. Unfortunately, naively applying Parikh's Theorem from classical automata theory to symbolic automata yields existential Presburger formulas of exponential size. We provide a new construction for Parikh's Theorem for symbolic automata and grammars, which avoids this exponential blowup: our algorithm computes an existential formula in polynomial-time over (quantifier-free) Presburger and the base theory. In fact, our algorithm extends to the model of parametric symbolic grammars, which are one of the most expressive models of languages over infinite alphabets. We have implemented our algorithm and show it can be used to solve string constraints that are difficult to solve by existing solvers.

cs.FL↗

arXiv2021

Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables

Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provide such a support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is undecidable, we show that our approach is complete for the so-called straight-line fragment. We evaluate the performance of our string solver on over 195000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods in both precision and efficiency.

cs.PL↗

arXiv2020

Collapsible Pushdown Parity Games

This paper studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes.

cs.FL↗

arXiv2020

A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type

Strings are widely used in programs, especially in web applications. Integer data type occurs naturally in string-manipulating programs, and is frequently used to refer to lengths of, or positions in, strings. Analysis and testing of string-manipulating programs can be formulated as the path feasibility problem: given a symbolic execution path, does there exist an assignment to the inputs that yields a concrete execution that realizes this path? Such a problem can naturally be reformulated as a string constraint solving problem. Although state-of-the-art string constraint solvers usually provide support for both string and integer data types, they mainly resort to heuristics without completeness guarantees. In this paper, we propose a decision procedure for a class of string-manipulating programs which includes not only a wide range of string operations such as concatenation, replaceAll, reverse, and finite transducers, but also those involving the integer data-type such as length, indexof, and substring. To the best of our knowledge, this represents one of the most expressive string constraint languages that is currently known to be decidable. Our decision procedure is based on a variant of cost register automata. We implement the decision procedure, giving rise to a new solver OSTRICH+. We evaluate the performance of OSTRICH+ on a wide range of existing and new benchmarks. The experimental results show that OSTRICH+ is the first string decision procedure capable of tackling finite transducers and integer constraints, whilst its overall performance is comparable with the state-of-the-art string constraint solvers.

cs.LO↗

arXiv2020

Monadic Decomposition in Integer Linear Arithmetic (Technical Report)

Monadic decomposability is a notion of variable independence, which asks whether a given formula in a first-order theory is expressible as a Boolean combination of monadic predicates in the theory. Recently, Veanes et al. showed the usefulness of monadic decomposability in the context of SMT (i.e. the input formula is quantifier-free), and found various interesting applications including string analysis. However, checking monadic decomposability is undecidable in general. Decidability for certain theories is known (e.g. Presburger Arithmetic, Tarski's Real-Closed Field), but there are very few results regarding their computational complexity. In this paper, we study monadic decomposability of integer linear arithmetic in the setting of SMT. We show that this decision problem is coNP-complete and, when monadically decomposable, a formula admits a decomposition of exponential size in the worst case. We provide a new application of our results to string constraint solving with length constraints. We then extend our results to variadic decomposability, where predicates could admit multiple free variables (in contrast to monadic decomposability). Finally, we give an application to quantifier elimination in integer linear arithmetic where the variables in a block of quantifiers, if independent, could be eliminated with an exponential (instead of the standard doubly exponential) blow-up.

cs.LO↗

arXiv2018

CSS Minification via Constraint Solving (Technical Report)

Minification is a widely-accepted technique which aims at reducing the size of the code transmitted over the web. We study the problem of minifying Cascading Style Sheets (CSS) --- the de facto language for styling web documents. Traditionally, CSS minifiers focus on simple syntactic transformations (e.g. shortening colour names). In this paper, we propose a new minification method based on merging similar rules in a CSS file. We consider safe transformations of CSS files, which preserve the semantics of the CSS file. The semantics of CSS files are sensitive to the ordering of rules in the file. To automatically identify a rule merging opportunity that best minimises file size, we reduce the rule-merging problem to a problem on CSS-graphs, i.e., node-weighted bipartite graphs with a dependency ordering on the edges, where weights capture the number of characters (e.g. in a selector or in a property declaration). Roughly speaking, the corresponding CSS-graph problem concerns minimising the total weight of a sequence of bicliques (complete bipartite subgraphs) that covers the CSS-graph and respects the edge order. We provide the first full formalisation of CSS3 selectors and reduce dependency detection to satisfiability of quantifier-free integer linear arithmetic, for which highly-optimised SMT-solvers are available. To solve the above NP-hard graph optimisation problem, we show how Max-SAT solvers can be effectively employed. We have implemented our algorithms using Max-SAT and SMT-solvers as backends, and tested against approximately 70 real-world examples (including the top 20 most popular websites). In our benchmarks, our tool yields larger savings than six well-known minifiers (which do not perform rule-merging, but support many other optimisations). Our experiments also suggest that better savings can be achieved in combination with one of these six minifiers.

cs.LO↗

arXiv2018

Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations

The design and implementation of decision procedures for checking path feasibility in string-manipulating programs is an important problem, whose applications include symbolic execution and automated detection of cross-site scripting (XSS) vulnerabilities. A (symbolic) path is a finite sequence of assignments and assertions (i.e. without loops), and checking its feasibility amounts to determining the existence of inputs that yield a successful execution. We give two general semantic conditions which together ensure the decidability of path feasibility: (1) each assertion admits regular monadic decomposition, and (2) each assignment uses a (possibly nondeterministic) function whose inverse relation preserves regularity. We show these conditions are expressive since they are satisfied by a multitude of string operations. They also strictly subsume existing decidable string theories, and most existing benchmarks (e.g. most of Kaluza's, and all of SLOG's, Stranger's, and SLOTH's). We give a simple decision procedure and an extensible architecture of a string solver in that a user may easily incorporate his/her own string functions. We show the general fragment has a tight, but high complexity. To address this, we propose to allow only partial string functions (i.e., prohibit nondeterminism) in condition (2). When nondeterministic functions are needed, we also provide a syntactic fragment that provides a support of nondeterministic functions but can be reduced to an existing solver SLOTH. We provide an efficient implementation of our decision procedure for deterministic partial string functions in a new string solver OSTRICH. It provides built-in support for concatenation, reverse, functional transducers, and replaceall and provides a framework for extensibility to support further string functions. We demonstrate the efficacy of our new solver against other competitive solvers.

cs.FL↗

arXiv2018

C-SHORe: Higher-Order Verification via Collapsible Pushdown System Saturation

Higher-order recursion schemes (HORS) have received much attention as a useful abstraction of higher-order functional programs with a number of new verification techniques employing HORS model-checking as their centrepiece. We give an account of the C-SHORe tool, which contributed to the ongoing quest for a truly scalable model-checker for HORS by offering a different, automata theoretic perspective. C-SHORe implements the first practical model-checking algorithm that acts on a generalisation of pushdown automata equi-expressive with HORS called collapsible pushdown systems (CPDS). At its core is a backwards saturation algorithm for CPDS. Additionally, it is able to use information gathered from an approximate forward reachability analysis to guide its backward search. Moreover, it uses an algorithm that prunes the CPDS prior to model-checking and a method for extracting counter-examples in negative instances. We provide an up-to-date comparison of C-SHORe with the state-of-the-art verification tools for HORS. The tool and additional material are available from http://cshore.cs.rhul.ac.uk.

cs.LO↗

arXiv2018

Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems

We give a direct polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games played over the same class of graphs. That a polynomial-time reduction would exist was known since both problems are complete for the same complexity class. Coming up with a direct reduction, however, has been an open problem. Our solution to the puzzle brings together a number of techniques for pushdown games and adds three new ones. This work contributes to a recent trend of liveness to safety reductions which allow the advanced state-of-the-art in safety checking to be used for more expressive specifications.

cs.LO↗

arXiv2018

Emptiness of Stack Automata is NEXPTIME-complete: A Correction

A saturation algorithm for collapsible pushdown systems was published in ICALP 2012. This work introduced a class of stack automata used to recognised regular sets of collapsible pushdown configurations. It was shown that these automata form an effective boolean algebra, have a linear time membership problem, and are equivalent to an alternative automata representation appearing in LICS 2010. It was also claimed that the emptiness problem for stack automata is PSPACE-complete. Unfortunately, this claim is not true. We show that the problem is in fact NEXPTIME-complete when the stacks being accepted are collapsible pushdown stacks, rather than the annotated stacks used in ICALP 2012.

cs.FL↗

arXiv2017

What Is Decidable about String Constraints with the ReplaceAll Function

Recently, it was shown that any theory of strings containing the string-replace function (even the most restricted version where pattern/replacement strings are both constant strings) becomes undecidable if we do not impose some kind of straight-line (aka acyclicity) restriction on the formulas. Despite this, the straight-line restriction is still practically sensible since this condition is typically met by string constraints that are generated by symbolic execution. In this paper, we provide the first systematic study of straight-line string constraints with the string-replace function and the regular constraints as the basic operations. We show that a large class of such constraints (i.e. when only a constant string or a regular expression is permitted in the pattern) is decidable. We note that the string-replace function, even under this restriction, is sufficiently powerful for expressing the concatenation operator and much more (e.g. extensions of regular expressions with string variables). This gives us the most expressive decidable logic containing concatenation, replace, and regular constraints under the same umbrella. Our decision procedure for the straight-line fragment follows an automata-theoretic approach, and is modular in the sense that the string-replace terms are removed one by one to generate more and more regular constraints, which can then be discharged by the state-of-the-art string constraint solvers. We also show that this fragment is, in a way, a maximal decidable subclass of the straight-line fragment with string-replace and regular constraints. To this end, we show undecidability results for the following two extensions: (1) variables are permitted in the pattern parameter of the replace function, (2) length constraints are permitted.

cs.LO↗

arXiv2017

Domains for Higher-Order Games

We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed-point computations can be applied.

cs.LO↗

arXiv2016

Decidable models of integer-manipulating programs with recursive parallelism (technical report)

We study safety verification for multithreaded programs with recursive parallelism (i.e. unbounded thread creation and recursion) as well as unbounded integer variables. Since the threads in each program configuration are structured in a hierarchical fashion, our model is state-extended ground-tree rewrite systems equipped with shared unbounded integer counters that can be incremented, decremented, and compared against an integer constant. Since the model is Turing-complete, we propose a decidable underapproximation. First, using a restriction similar to context-bounding, we underapproximate the global control by a weak global control (i.e. DAGs possibly with self-loops), thereby limiting the number of synchronisations between different threads. Second, we bound the number of reversals between non-decrementing and non-incrementing modes of the counters. Under this restriction, we show that reachability becomes NP-complete. In fact, it is poly-time reducible to satisfaction over existential Presburger formulas, which allows one to tap into highly optimised SMT solvers. Our decidable approximation strictly generalises known decidable models including (i) weakly-synchronised ground-tree rewrite systems, and (ii) synchronisation/reversal-bounded concurrent pushdown systems systems with counters. Finally, we show that, when equipped with reversal-bounded counters, relaxing the weak control restriction by the notion of senescence results in undecidability.

cs.LO↗

arXiv2016

Generating Concurrency Checks Automatically

This article introduces ATAB, a tool that automatically generates pairwise reachability checks for action trees. Action trees can be used to study the behaviour of real-world concurrent programs. ATAB encodes pairwise reachability checks into alternating tree automata that determine whether an action tree has a schedule where any pair of given points in the program are simultaneously reachable. Because the pairwise reachability problem is undecidable in general ATAB operates under a restricted form of lock-based concurrency. ATAB produces alternating tree automata that are more compact and more efficiently checkable than those that have been previously used. The process is entirely automated, which simplifies the process of encoding checks for more complex action trees. The alternating tree automata produced are easier to scale to large numbers of locks than previous constructions.

cs.LO↗