Author name cluster

Joel D. Day

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

TCS Journal 2023 Journal Article

Towards more efficient methods for solving regular-expression heavy string constraints

Murphy Berzish
Joel D. Day
Vijay Ganesh
Mitja Kulczynski
Florin Manea
Federico Mora
Dirk Nowotka

Widespread use of string solvers in the formal analysis of string-heavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this context. Designing practical algorithms for the (generally undecidable) satisfiability problem for systems of string constraints requires a deep understanding of the structure of constraints present in the targeted cases. In this paper, we first investigate relevant benchmarks containing regular expression membership predicates, extract a series of first order logic theories, and prove the decidability, respectively undecidability, of their satisfiability problem. Further, building on the theoretical results, we present a novel length-aware solving algorithm for the quantifier-free first-order theory over regular expression membership predicates and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. Besides the theoretical aspects leading to this algorithm, a crucial insight that underpins it is that real-world regex and string formulas contain a wealth of information about upper and lower bounds on lengths of strings, and such information can be used very effectively to simplify operations on automata representing regular expressions. Additionally, we present several novel general heuristics, such as the prefix/suffix method, that can be used to make a variety of regex solving algorithms more efficient in practice. We showcase the power of our algorithm and heuristics via an extensive empirical evaluation over a large and diverse benchmark of 57256 regex-heavy instances, almost 75% of which are derived from industrial applications or contributed by other solver developers. Our solver outperforms five other state-of-the-art string solvers over this benchmark.

Details DOI

I&C Journal 2022 Journal Article

Unambiguous injective morphisms in free groups

Joel D. Day
Daniel Reidenbach

A morphism g is ambiguous with respect to a word u if there exists a second morphism h ≠ g such that g ( u ) = h ( u ). Otherwise g is unambiguous with respect to u. Thus unambiguous morphisms are those for which the structure of the morphism is preserved in the image. Ambiguity has so far been studied for morphisms of free monoids, where several characterisations exist for the set of words u permitting an (injective) unambiguous morphism. In the present paper, we consider ambiguity of morphisms of free groups, and consider possible analogies to the existing characterisations in the free monoid. While a direct generalisation results in a trivial situation where all morphisms are ambiguous, we discuss some natural and well-motivated reformulations, and provide a characterisation of words in a free group that permit a morphism which is “as unambiguous as possible”.

Details DOI

FormaliSE Conference 2020 Conference Paper

Rule-based Word Equation Solving

Joel D. Day
Mitja Kulczynski
Florin Manea
Dirk Nowotka
Danny Bøgsted Poulsen

We present a transformation-system-based technique in the framework of string solving, by reformulating a classical combinatorics on words result, the Lemma of Levi. We further enrich the induced rules by simplification steps based on results from the combinatorial theory of word equations, as well as by the addition of linear length constraints. This transformation-system approach cannot solve all equations efficiently by itself. To improve the efficiency of our transformation-system approach we integrate existing successful string solvers, which are called based on several heuristics. The experimental evaluation we performed shows that integrating our technique as an inprocessing step improves in general the performance of existing solvers.

Details

MFCS Conference 2019 Conference Paper

Upper Bounds on the Length of Minimal Solutions to Certain Quadratic Word Equations

Joel D. Day
Florin Manea
Dirk Nowotka

It is a long standing conjecture that the problem of deciding whether a quadratic word equation has a solution is in NP. It has also been conjectured that the length of a minimal solution to a quadratic equation is at most exponential in the length of the equation, with the latter conjecture implying the former. We show that both conjectures hold for some natural subclasses of quadratic equations, namely the classes of regular-reversed, k-ordered, and variable-sparse quadratic equations. We also discuss a connection of our techniques to the topic of unavoidable patterns, and the possibility of exploiting this connection to produce further similar results.

Details

MFCS Conference 2017 Conference Paper

The Hardness of Solving Simple Word Equations

Joel D. Day
Florin Manea
Dirk Nowotka

We investigate the class of regular-ordered word equations. In such equations, each variable occurs at most once in each side and the order of the variables occurring in both left and right hand sides is preserved (the variables can be, however, separated by potentially distinct constant factors). Surprisingly, we obtain that solving such simple equations, even when the sides contain exactly the same variables, is NP-hard. By considerations regarding the combinatorial structure of the minimal solutions of the more general quadratic equations we obtain that the satisfiability problem for regular-ordered equations is in NP. The complexity of solving such word equations under regular constraints is also settled. Finally, we show that a related class of simple word equations, that generalises one-variable equations, is in P.

Details

TCS Journal 2015 Journal Article

Periodicity forcing words

Joel D. Day
Daniel Reidenbach
Johannes C. Schneider

The Dual Post Correspondence Problem asks, for a given word α, if there exists a non-periodic morphism g and an arbitrary morphism h such that g ( α ) = h ( α ). Thus α satisfies the Dual PCP if and only if it belongs to a non-trivial equality set. Words which do not satisfy the Dual PCP are called periodicity forcing, and are important to the study of word equations, equality sets and ambiguity of morphisms. In this paper, a ‘prime’ subset of periodicity forcing words is presented. It is shown that when combined with a particular type of morphism it generates exactly the full set of periodicity forcing words. Furthermore, it is shown that there exist examples of periodicity forcing words which contain any given factor/prefix/suffix. Finally, an alternative class of mechanisms for generating periodicity forcing words is developed, resulting in a class of examples which contrast those known already.

Details DOI