arxiv: 2605.14872 · v1 · submitted 2026-05-14 · 💻 cs.FL · cs.LO

Recognition: 2 theorem links

· Lean Theorem

String Solving with Stabilization and Transducers (Technical Report)

David Chocholat\'y , Vojt\v{e}ch Havlena , Luk\'a\v{s} Hol\'ik , Ond\v{r}ej Leng\'al , Juraj S\'i\v{c} , Michal \v{S}ed\'y

Authors on Pith no claims yet

Pith reviewed 2026-05-15 03:01 UTC · model grok-4.3

classification 💻 cs.FL cs.LO

keywords string constraint solvingfinite-state transducersstabilization methodrelational constraintslength constraintsautomata-based solvingheuristicsreplaceAll

0 comments

The pith

Generalizing stabilization to transducers handles relational string constraints efficiently by reducing costly length operations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends the stabilization-based automata method from Z3-Noodler to support relational constraints modeled by finite-state transducers. It reduces reliance on expensive concatenation elimination when handling length constraints and introduces heuristics for better practical results. The implementation solves more benchmark instances than prior solvers and achieves orders of magnitude speedups on relational constraint problems. This matters because relational operations like replaceAll appear frequently in real string programs yet remain hard for existing solvers.

Core claim

The stabilization method is generalized to finite-state transducers for relational constraints, with reductions that lessen the reliance on concatenation elimination for length constraints, supplemented by heuristics that improve solving efficiency in practice.

What carries the argument

Finite-state transducers integrated into the stabilization-based automata approach for modeling relational string operations, paired with length constraint reductions that avoid full concatenation elimination.

If this is right

Relational operations such as replaceAll become practically solvable in automata-based string solvers.
Fewer calls to concatenation elimination lead to better scaling on large or complex length constraints.
Heuristics yield measurable reductions in runtime on standard benchmark suites.
The solver now covers more instances with relational constraints than previous tools.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The transducer approach could be extended to additional string operations by composing more complex transducers without changing the core stabilization loop.
Similar length reductions might apply to other automata-based solvers outside the stabilization family.
Performance gains on relational benchmarks suggest that transducer encodings could become a standard building block for SMT string theories.
Composing multiple transducers before stabilization might further cut the cost of relational chains.

Load-bearing premise

The transducer encodings and length constraint reductions preserve soundness and completeness while the heuristics do not miss solutions on realistic inputs.

What would settle it

A concrete relational string constraint instance on which the new solver returns an incorrect satisfiability result or solution that a sound reference solver would refute.

Figures

Figures reproduced from arXiv: 2605.14872 by David Chocholat\'y, Juraj S\'i\v{c}, Luk\'a\v{s} Hol\'ik, Michal \v{S}ed\'y, Ond\v{r}ej Leng\'al, Vojt\v{e}ch Havlena.

**Figure 1.** Figure 1: Transducer T for vz = replaceAll(xy, <, <). shortest non-empty match of L in ν(t) by w. We note that if L = {w ′} is a singleton language, we abuse notation and write replaceAll(t, w, w′ ). replaceAll operations can also be nested (the subject t can itself be an application of a replaceAll operation), allowing, for instance, to specify character encoding by its HTML codes. We use the techniques of [… view at source ↗

**Figure 2.** Figure 2: Examples of inclusion graphs. (a) An acyclic inclusion graph for a chain-free [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

**Figure 3.** Figure 3: Compositional transducer T+ constructed during concatenation-eliminating noodlification for constraint in Example 4. The non-dashed part is one of its noodles. of t (with output delimiter ▷). Intuitively, L(T) would have a word w ∈ (Σ2 ϵ ) ∗ encoding a pair (u, v) with u = ux1 · · · uxn ∈ Reg(s) and v = vy1 · · · vym ∈ Reg(t). The split of w into the concatenation of segments wi0,j0 · . . . · win+m,jn+m w… view at source ↗

**Figure 4.** Figure 4: Elements of ψ. Example 4 . Let Σ = {a, <, &, l, t, ; } be an alphabet, φ = Reg ∧ T(xy, vz) a cube where T is the transducer from Section 2, replacing all occurrences of < with <. We use the standard regular expressions to define regular languages. Reg is given as Reg(x) = [alt]+< ∗ , Reg(y) = < ∗[;&]∗ , Reg(v) = (at)∗ (&lt)+, and Reg(z) = ; ∗& ∗ [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗

**Figure 5.** Figure 5: T(x, y, z) Example 7. Consider the 3-tape transducer T(x, y, z) over the single dummy symbol # shown right. Each transition label a1/a2/a3 indicates what is read on tapes x, y, z, respectively. Let n1, n2, n3 ≥ 0 count how many times the lower (ε/ε/#), middle (#/#/#), and upper (ε/#/ε) transition is taken. Then, the Parikh image of T is given as ∃n1, n2, n3 ≥ 0: lenx = n2∧leny = n2 +n3∧lenz = n1 +n2∧n1 +n3… view at source ↗

**Figure 6.** Figure 6: Comparison with cvc5, Z3, and OSTRICH. Times are in seconds, axes are logarithmic. Colors distinguish benchmark sets: • PCP, • RNA, • Transducer+, and • Webapp [PITH_FULL_IMAGE:figures/full_fig_p022_6.png] view at source ↗

**Figure 7.** Figure 7: Elements of ψp. Example 8. Consider the formula φ: T(x, x) ∧ x ∈ {ab, ba} ∧ Len where T is a transducer recognizing the relation {(ab, ba),(ba, ab)}, and Len are some length constraints where x is a length variable. Notice that formula φ has no solution since both sides of T comprise of only x, hence need to be equal, which contradicts the relation recognized by T. However, if we construct T+ and derive… view at source ↗

read the original abstract

We generalize an efficient automata-based approach to string constraint solving, the stabilization-based method behind the solver Z3-Noodler, to support relational constraints represented by finite-state transducers (useful, for example, for modeling replaceAll constraints). We focus on an efficient treatment of length constraints by reducing the need for expensive concatenation elimination, which is a major bottleneck in automata-based string solving. We also propose powerful heuristics that significantly improve performance in practice. Implemented on top of Z3-Noodler, our method vastly outperforms existing solvers on benchmarks with relational constraints. It solves more instances and runs orders of magnitude faster.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Extends stabilization to transducers for relational constraints and cuts concatenation work via length handling, with good benchmark gains but weak completeness case for the heuristics.

read the letter

The paper generalizes the stabilization method from Z3-Noodler to finite-state transducers so it can handle relational string constraints like replaceAll. It also introduces length-constraint reductions meant to avoid full concatenation elimination and adds some heuristics for speed. These are the concrete advances over the prior work it builds on. The implementation reports clear wins on benchmarks with relational constraints, solving more instances and running much faster than other solvers. That practical result is the part worth paying attention to if you work with string solvers in verification or security tools. The transducer encoding itself looks like a straightforward lift of the automata approach, and the length reductions target a real bottleneck. The soft spot is the lack of a clear completeness argument for the combined system. The length reductions and heuristics are presented as preserving solutions while pruning only unsat branches, but without a proof sketch or separate argument showing they do not miss cases under transducer composition, the performance claims rest on experimental evidence alone. If those steps implicitly rely on bounds that fail in some realistic inputs, the solver could return wrong answers. The experiments are described as strong, but the abstract gives no error bars or setup details to assess variance. This is aimed at people building or extending string solvers for program analysis. A reader already familiar with automata-based constraint solving would get the most from the transducer and length details. It deserves peer review because the core extension is technically plausible and the reported gains are large enough to check, even if the formal side needs tightening.

Referee Report

2 major / 2 minor

Summary. The paper generalizes the stabilization-based string constraint solving technique from Z3-Noodler to handle relational constraints encoded by finite-state transducers. It reduces reliance on expensive concatenation elimination through specialized length-constraint handling and introduces new heuristics, claiming that the resulting implementation solves more instances and runs orders of magnitude faster than existing solvers on benchmarks containing relational constraints.

Significance. If the transducer reductions and heuristics preserve soundness and completeness, the work would constitute a meaningful practical advance in automata-based string solving by extending an already efficient stabilization framework to a broader class of constraints (e.g., replaceAll) while mitigating a known bottleneck. The direct implementation on top of Z3-Noodler and the focus on length constraints are concrete strengths that could translate into improved performance for verification and program-analysis applications.

major comments (2)

[Abstract] Abstract and the description of the transducer encoding: the central performance claim rests on the assertion that the new transducer handling and length-constraint reductions preserve all solutions. No soundness or completeness argument is supplied for the combined system; if the length reductions implicitly rely on bounds that fail for certain transducer compositions, or if the heuristics discard feasible paths, the solver could return incorrect unsat answers. This directly undermines the claim that the method 'vastly outperforms ... while remaining correct.'
[Length-constraint handling] The section on length-constraint reductions: the paper states that these reductions avoid concatenation elimination, yet provides no formal argument or invariant showing that the reductions are equivalence-preserving when transducers are present. Without such an argument the experimental superiority cannot be interpreted as evidence of a correct algorithm.

minor comments (2)

[Abstract] The abstract refers to 'powerful heuristics' without naming them or indicating their scope; a brief enumeration in the abstract or introduction would improve readability.
[Experimental evaluation] Benchmark results are summarized qualitatively ('orders of magnitude faster') but lack any table or figure reference in the provided text; explicit cross-references to experimental tables would strengthen the presentation.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and for identifying the need to make the soundness arguments more explicit. We address the two major comments point by point below. In both cases we agree that additional formal material is required and will incorporate it in the revision.

read point-by-point responses

Referee: [Abstract] Abstract and the description of the transducer encoding: the central performance claim rests on the assertion that the new transducer handling and length-constraint reductions preserve all solutions. No soundness or completeness argument is supplied for the combined system; if the length reductions implicitly rely on bounds that fail for certain transducer compositions, or if the heuristics discard feasible paths, the solver could return incorrect unsat answers. This directly undermines the claim that the method 'vastly outperforms ... while remaining correct.'

Authors: The transducer encoding is realized by synchronous composition of the input transducer with the stabilized automata; because both the original stabilization procedure and the transducer operations are language-preserving, the set of solutions is unchanged. Length bounds are obtained by projecting the length automaton through the same composition, inheriting the tightness guarantees of the base method. The heuristics only reorder reduction steps and never prune feasible paths; any path that would be explored in the unguided algorithm remains reachable. We acknowledge that the manuscript does not contain a self-contained proof of these facts and will add a dedicated subsection (with lemmas) establishing language equivalence and length preservation for the combined system. The abstract will be revised to reference this argument. revision: yes
Referee: [Length-constraint handling] The section on length-constraint reductions: the paper states that these reductions avoid concatenation elimination, yet provides no formal argument or invariant showing that the reductions are equivalence-preserving when transducers are present. Without such an argument the experimental superiority cannot be interpreted as evidence of a correct algorithm.

Authors: The length reductions operate on the minimal and maximal lengths extracted from the product automaton obtained after transducer composition. Because the product construction preserves the exact set of strings (and therefore their lengths), the extracted bounds remain equivalent to those of the original constraint. We agree that an explicit invariant relating the reduced length constraints to the original transducer-augmented formula is missing from the current text. In the revision we will insert a short invariant statement together with a proof sketch that the reductions are satisfiability-preserving, relying only on standard properties of automata projection and the stabilization fixed-point. revision: yes

Circularity Check

0 steps flagged

No significant circularity in the algorithmic derivation

full rationale

The paper describes an extension of the prior stabilization method (from Z3-Noodler) to transducers for relational constraints, plus length-constraint reductions and heuristics. Performance claims rest on empirical benchmark results rather than any mathematical derivation, equation, or prediction that reduces by construction to the paper's own inputs, fitted parameters, or self-referential definitions. The stabilization reference is external prior work; the new transducer encodings, concatenation-elimination reductions, and heuristics are presented as independent additions without load-bearing self-citation chains or ansatzes smuggled via citation. This is a standard implementation paper whose central claims are falsifiable via benchmarks and do not collapse to tautology.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The method rests on standard automata theory; no free parameters, invented entities, or ad-hoc axioms are described in the abstract.

axioms (1)

standard math Standard closure and decision properties of finite automata and transducers
The stabilization and transducer constructions presuppose that automata operations remain effective for the string constraints considered.

pith-pipeline@v0.9.0 · 5431 in / 1108 out tokens · 47698 ms · 2026-05-15T03:01:36.414749+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We generalize an efficient automata-based approach to string constraint solving—the stabilization-based method behind the solver Z3-Noodler—to support relational constraints represented by finite-state transducers
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

The length image LenImg(ψ) of a formula ψ is a LIA formula over variables {len x | x ∈ Var(ψ)} that characterizes the lengths of the solutions of ψ

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

50 extracted references · 50 canonical work pages

[1]

SMT-COMP QF Strings, 2024 (2024),https://smt-comp.github.io/2024/ results/qf_strings-single-query/,https://smt-comp.github.io/2024/ results/qf_strings-single-query/

work page 2024
[2]

SMT-COMP QF Strings, 2025 (2025),https://smt-comp.github.io/2025/ results/qf_slia-single-query/,https://smt-comp.github.io/2025/ results/qf_slia-single-query/

work page 2025
[3]

In: Co- hen, A., Vechev, M.T

Abdulla, P.A., Atig, M.F., Chen, Y., Diep, B.P., Hol´ ık, L., Rezine, A., R¨ ummer, P.: Flatten and conquer: a framework for efficient analysis of string constraints. In: Co- hen, A., Vechev, M.T. (eds.) Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017. pp. 602–...

work page doi:10.1145/3062341.3062384 2017
[4]

In: Biere, A., Bloem, R

Abdulla, P.A., Atig, M.F., Chen, Y., Hol´ ık, L., Rezine, A., R¨ ummer, P., Sten- man, J.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) Com- puter Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18- 22, 2014. Proceedings. Lecture Notes in Comp...

work page 2014
[5]

Springer (2014).https://doi.org/10.1007/978-3-319-08867-9_10,https: //doi.org/10.1007/978-3-319-08867-9_10

work page doi:10.1007/978-3-319-08867-9_10 2014
[6]

In: Chen, Y., Cheng, C., Esparza, J

Abdulla, P.A., Atig, M.F., Diep, B.P., Hol´ ık, L., Jank˚ u, P.: Chain-free string constraints. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technol- ogy for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11781, pp. 277–293. Springer (2...

work page doi:10.1007/978-3-030-31784-3_16 2019
[7]

In: 2018 Formal Methods in Computer Aided Design (FMCAD)

Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for aws access policies using smt. In: 2018 Formal Methods in Computer Aided Design (FMCAD). pp. 1–9 (2018).https://doi.org/10.23919/FMCAD.2018.8602994

work page doi:10.23919/fmcad.2018.8602994 2018
[8]

In: Fisman, D., Rosu, G

Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mo- hamed, A., Mohamed, M., Niemetz, A., N¨ otzli, A., Ozdemir, A., Preiner, M., 24 Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial- strength smt solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of System...

work page 2022
[9]

shtml(2025)

Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Li- brary (SMT-LIB): Strings.https://smt-lib.org/theories-UnicodeStrings. shtml(2025)

work page 2025
[10]

Berzish, M., Day, J.D., Ganesh, V., Kulczynski, M., Manea, F., Mora, F., Nowotka, D.: Towards more efficient methods for solving regular-expression heavy string constraints. Theor. Comput. Sci.943, 50–72 (2023).https://doi.org/10.1016/ j.tcs.2022.12.009,https://doi.org/10.1016/j.tcs.2022.12.009

work page doi:10.1016/j.tcs.2022.12.009 2023
[11]

In: Stewart, D., Weissenbacher, G

Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: A string solver with theory-aware heuristics. In: 2017 Formal Methods in Computer Aided Design (FMCAD). pp. 55–59 (2017).https://doi.org/10.23919/FMCAD.2017.8102241

work page doi:10.23919/fmcad.2017.8102241 2017
[12]

In: Silva, A., Leino, K.R.M

Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J.D., Nowotka, D., Ganesh, V.: An SMT solver for regular expressions and linear arithmetic over string length. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification - 33rd Interna- tional Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Lecture Notes in Computer S...

work page doi:10.1007/978-3-030-81688-9_14 2021
[13]

Berzish, Murphy: Z3str4: A Solver for Theories over Strings. Ph.D. thesis (2021), http://hdl.handle.net/10012/17102

work page 2021
[14]

In: Chechik, M., Ka- toen, J.P., Leucker, M

Blahoudek, F., Chen, Y.F., Chocholat´ y, D., Havlena, V., Hol´ ık, L., Leng´ al, O., S´ ıˇ c, J.: Word equations in synergy with regular constraints. In: Chechik, M., Ka- toen, J.P., Leucker, M. (eds.) Formal Methods. pp. 403–423. Springer International Publishing, Cham (2023)

work page 2023
[15]

Constraints (May 2025).https://doi.org/10.1007/s10601-025-09379-w, https://doi.org/10.1007/s10601-025-09379-w

Blahoudek, F., Chen, Y.F., Chocholat´ y, D., Havlena, V., Hol´ ık, L., Leng´ al, O., S´ ıˇ c, J.: Word equations in synergy with regular constraints (extended ver- sion). Constraints (May 2025).https://doi.org/10.1007/s10601-025-09379-w, https://doi.org/10.1007/s10601-025-09379-w

work page doi:10.1007/s10601-025-09379-w 2025
[16]

Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z.: What is decidable about string constraints with the replaceall function. Proc. ACM Program. Lang.2(POPL), 3:1–3:29 (2018).https://doi.org/10.1145/3158091,https://doi.org/10.1145/ 3158091

work page doi:10.1145/3158091 2018
[17]

Chen, T., Flores-Lamas, A., Hague, M., Han, Z., Hu, D., Kan, S., Lin, A.W., R¨ ummer, P., Wu, Z.: Solving string constraints with regex-dependent functions through transducers with priorities and variables. Proc. ACM Program. Lang. 6(POPL), 1–31 (2022).https://doi.org/10.1145/3498707,https://doi.org/ 10.1145/3498707

work page doi:10.1145/3498707 2022
[18]

In: Hung, D.V., Sokolsky, O

Chen, T., Hague, M., He, J., Hu, D., Lin, A.W., R¨ ummer, P., Wu, Z.: A decision procedure for path feasibility of string manipulating programs with integer data type. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, Oc- tober 19-23, 2020, Proceedings. Lecture...

work page doi:10.1007/978-3-030-59152-6_ 2020
[19]

Chen, T., Hague, M., Lin, A.W., R¨ ummer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang.3(POPL), 49:1–49:30 (2019).https://doi.org/10.1145/ 3290362,https://doi.org/10.1145/3290362 25

work page doi:10.1145/3290362 2019
[20]

In: Finkbeiner, B., Kov´ acs, L

Chen, Y.F., Chocholat´ y, D., Havlena, V., Hol´ ık, L., Leng´ al, O., S´ ıˇ c, J.: Z3-Noodler: An automata-based string solver. In: Finkbeiner, B., Kov´ acs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 24–33. Springer Nature Switzerland, Cham (2024)

work page 2024
[21]

Chen, Y.F., Chocholat´ y, D., Havlena, V., Heˇ cko, M., Hol´ ık, L., Leng´ al, O., S´ ıˇ c, J.: Z3-noodler: An automata-based smt string solver.https://github.com/VeriFIT/ z3-noodler(2026)

work page 2026
[22]

Chen, Y.F., Chocholat´ y, D., Havlena, V., Hol´ ık, L., Leng´ al, O., S´ ıˇ c, J.: Solv- ing string constraints with lengths by stabilization. Proc. ACM Program. Lang. 7(OOPSLA2) (oct 2023).https://doi.org/10.1145/3622872

work page doi:10.1145/3622872 2023
[23]

In: Tools and Algorithms for the Construction and Analysis of Systems

Chocholat´ y, D., Havlena, V., Hol´ ık, L., Hraniˇ cka, J., Leng´ al, O., S´ ıˇ c, J.: Z3-Noodler 1.3: Shepherding decision procedures for strings with model generation. In: Tools and Algorithms for the Construction and Analysis of Systems. Springer Nature Switzerland, Cham (2025)

work page 2025
[24]

org/10.5281/zenodo.19814331,https://doi.org/10.5281/zenodo.19814331

Chocholat´ y, D., Havlena, V., Hol´ ık, L., S´ ıˇ c, J.,ˇSed´ y, M.: Artifact for the cav’26 pa- per ”string solving with stabilization and transducers” (Apr 2026).https://doi. org/10.5281/zenodo.19814331,https://doi.org/10.5281/zenodo.19814331

work page doi:10.5281/zenodo.19814331 2026
[25]

In: Filiot, E., Jungers, R.M., Potapov, I

Day, J.D., Ehlers, T., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: On solving word equations using SAT. In: Filiot, E., Jungers, R.M., Potapov, I. (eds.) Reachability Problems - 13th International Conference, RP 2019, Brus- sels, Belgium, September 11-13, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11674, pp. 93–106. Springer (20...

work page doi:10.1007/978-3-030-30806-3_8 2019
[26]

Day, J.D., Ganesh, V., Grewal, N., Manea, F.: On the expressive power of string constraints. Proc. ACM Program. Lang.7(POPL), 278–308 (2023).https://doi. org/10.1145/3571203,https://doi.org/10.1145/3571203

work page doi:10.1145/3571203 2023
[27]

In: Pozzato, G.L., Uustalu, T

Eisenhofer, C., Seiser, T., Bjørner, N., Kov´ acs, L.: On solving string equations via powers and parikh images. In: Pozzato, G.L., Uustalu, T. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. pp. 120–138. Springer Nature Switzerland, Cham (2026)

work page 2026
[28]

In: Mu˜ noz, C.A

Fu, X., Li, C.: Modeling regular replacement for string constraint solving. In: Mu˜ noz, C.A. (ed.) Second NASA Formal Methods Symposium - NFM 2010, Wash- ington D.C., USA, April 13-15, 2010. Proceedings. NASA Conference Proceedings, vol. NASA/CP-2010-216215, pp. 67–76 (2010)

work page 2010
[29]

In: Irfan, A., Kaufmann, D

Hague, M., Hu, D., Je˙ z, A., Lin, A.W., Markgraf, O., R¨ ummer, P., Wu, Z.: OSTRICH2: Solver for complex string constraints. In: Irfan, A., Kaufmann, D. (eds.) Proceedings of the 25th Conference on Formal Methods in Computer- Aided Design – FMCAD 2025. pp. 145–158. TU Wien Academic Press (2025). https://doi.org/10.34727/2025/isbn.978-3-85448-084-6_21

work page doi:10.34727/2025/isbn.978-3-85448-084-6_21 2025
[30]

Hague, M., Je˙ z, A., Lin, A.W., Markgraf, O., R¨ ummer, P.: The power of regular constraint propagation. Proc. ACM Program. Lang.9(OOPSLA2) (Oct 2025). https://doi.org/10.1145/3763165,https://doi.org/10.1145/3763165

work page doi:10.1145/3763165 2025
[31]

In: Chakraborty, S., Jiang, J.H.R

Havlena, V., Hol´ ık, L., Leng´ al, O., S´ ıˇ c, J.: Cooking String-Integer Conversions with Noodles. In: Chakraborty, S., Jiang, J.H.R. (eds.) 27th International Con- ference on Theory and Applications of Satisfiability Testing (SAT 2024). Leib- niz International Proceedings in Informatics (LIPIcs), vol. 305, pp. 14:1–14:19. Schloss Dagstuhl – Leibniz-Ze...

work page doi:10.4230/lipics.sat.2024.14 2024
[32]

Hol´ ık, L., Jank˚ u, P., Lin, A.W., R¨ ummer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. Proc. ACM Program. Lang. 2(POPL), 4:1–4:32 (2018).https://doi.org/10.1145/3158092,https://doi. org/10.1145/3158092

work page doi:10.1145/3158092 2018
[33]

In: Piskac, R., Rakamari´ c, Z

Jiang, H., Lin, A.W., Markgraf, O., R¨ ummer, P., Stan, D.: HornStr: Invariant synthesis for regular model checking as constrained horn clauses. In: Piskac, R., Rakamari´ c, Z. (eds.) Computer Aided Verification. pp. 200–214. Springer Nature Switzerland, Cham (2025)

work page 2025
[34]

In: Bod´ ık, R., Majumdar, R

Lin, A.W., Barcel´ o, P.: String solving with word equations and transducers: to- wards a logic for analysing mutation XSS. In: Bod´ ık, R., Majumdar, R. (eds.) Pro- ceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 123–136. ACM (2016).https://doi...

work page doi:10.1145/2837614.2837641 2016
[35]

In: Marsland, T., Frank, I

Lorentz, R.J.: Creating difficult instances of the post correspondence problem. In: Marsland, T., Frank, I. (eds.) Computers and Games. pp. 214–228. Springer Berlin Heidelberg, Berlin, Heidelberg (2001)

work page 2001
[36]

In: CAV’23

Lotz, K., Goel, A., Dutertre, B., Kiesl-Reiter, B., Kong, S., Majumdar, R., Nowotka, D.: Solving string constraints using sat. In: CAV’23. pp. 187–208. Springer, Cham (2023)

work page 2023
[37]

In: Irfan, A., Kaufmann, D

Lotz, K., Kulczynski, M., Nowotka, D.: s2s: An eager SMT solver for strings. In: Irfan, A., Kaufmann, D. (eds.) Proceedings of the 25th Conference on Formal Meth- ods in Computer-Aided Design – FMCAD 2025. pp. 133–138. TU Wien Academic Press (2025).https://doi.org/10.34727/2025/isbn.978-3-85448-084-6_19

work page doi:10.34727/2025/isbn.978-3-85448-084-6_19 2025
[38]

Markgraf, O.: 4 different benchmark sets focused around str.replace all (2025), https://github.com/SMT-LIB/benchmark-submission/pull/7, GitHub pull re- quest

work page 2025
[39]

In: Tiuryn, J

Morvan, C.: On rational graphs. In: Tiuryn, J. (ed.) Foundations of Software Sci- ence and Computation Structures. pp. 252–266. Springer Berlin Heidelberg, Berlin, Heidelberg (2000)

work page 2000
[40]

In: TACAS’08

de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS’08. LNCS, vol. 4963, pp. 337–340. Springer (2008),https://doi.org/10.1007/ 978-3-540-78800-3_24

work page 2008
[41]

Myreen, M., Leng´ al, O.: Cav 2026 artifact evaluation vm - ubuntu 24.04.4 lts (Mar 2026).https://doi.org/10.5281/zenodo.19184839,https://doi.org/10.5281/ zenodo.19184839

work page doi:10.5281/zenodo.19184839 2026
[42]

In: Shoham, S., Vizel, Y

N¨ otzli, A., Reynolds, A., Barbosa, H., Barrett, C., Tinelli, C.: Even faster conflicts and lazier reductions for string solvers. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. pp. 205–226. Springer International Publishing, Cham (2022)

work page 2022
[43]

In: Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs

Omori, A., Minamide, Y.: Further tackling post correspondence problem and proof generation. In: Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs. p. 231–242. CPP ’25, Association for Comput- ing Machinery, New York, NY, USA (2025).https://doi.org/10.1145/3703595. 3705886,https://doi.org/10.1145/3703595.3705886

work page doi:10.1145/3703595 2025
[44]

Parikh, R.J.: On context-free languages. J. ACM13(4), 570–581 (oct 1966).https: //doi.org/10.1145/321356.321364,https://doi.org/10.1145/321356.321364

work page doi:10.1145/321356.321364 1966
[45]

Preiner, M., Schurr, H.J., Barrett, C., Fontaine, P., Niemetz, A., Tinelli, C.: SMT- LIB release 2025 (non-incremental benchmarks) (Aug 2025).https://doi.org/ 10.5281/zenodo.16740866,https://doi.org/10.5281/zenodo.16740866 27

work page doi:10.5281/zenodo.16740866 2025
[46]

In: Shoham, S., Vizel, Y

Rungta, N.: A billion SMT queries a day (invited paper). In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. Lecture Notes in Com- puter Science, vol. 13371, pp. 3–18. Springer (2022).https://doi.org/10.1007/ 978-3-031-13185-1_1,https://doi.org/10.10...

work page doi:10.1007/978-3-031-13185-1_1 2022
[47]

In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Stanford, C., Veanes, M., Bjørner, N.: Symbolic boolean derivatives for effi- ciently solving extended regular expression constraints. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. p. 620–635. PLDI 2021, Association for Computing Machin- ery, New York, NY, USA (2021).https://doi.org/10....

work page doi:10.1145/3453483.3454066 2021
[48]

Trinh, M., Chu, D., Jaffar, J.: S3: A symbolic string solver for vulnerability de- tection in web applications. In: CCS. pp. 1232–1243. ACM Trans. Comput. Log. (2014)

work page 2014
[49]

In: CAV’16

Trinh, M., Chu, D., Jaffar, J.: Progressive reasoning over recursively-defined strings. In: CAV’16. LNCS, vol. 9779, pp. 218–240. Springer (2016)

work page 2016
[50]

In: TACAS’10

Yu, F., Alkhalaf, M., Bultan, T.: Stranger: An automata-based string analysis tool for PHP. In: TACAS’10. LNCS, vol. 6015, pp. 154–157. Springer (2010) 28 A Proof of Lemma 1 Lemma 1.Our definition of a chain-free cube is equivalent to the definition of a positive chain-free cube in [5]. Proof (sketch).The equivalence of the chain-free definition using an ...

work page 2010