String Solving with Stabilization and Transducers
Computer Aided Verification (CAV 2026), LNCS 16683, pp. 50–74, Springer · Lisbon, Portugal
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.
@inproceedings{ChocholatyHHSS26,
author = {David Chocholat{\'y} and Vojt{\v{e}}ch Havlena and
Luk{\'a}{\v{s}} Hol{\'i}k and Juraj S{\'i}{\v{c}} and
Michal {\v{S}}ed{\'y}},
title = {String Solving with Stabilization and Transducers},
booktitle = {Computer Aided Verification -- 38th International
Conference, {CAV} 2026},
series = {Lecture Notes in Computer Science},
volume = {16683},
pages = {50--74},
publisher = {Springer},
year = {2026},
doi = {10.1007/978-3-032-32526-6_3}
}