Solving String Constraints with Lengths by Stabilization
summary
Combines a fast automata-based stabilization solver for equations+regular constraints with an align-and-split module to extract lengths, implements both in Z3 Noodler backed by the new automata library Mata, and solves unrestricted disequalities and length arithmetic to extend the chain‑free decidable fragment. Evaluation shows fewer unsolved instances and lower average times on SMT-LIB benchmarks; pairing Z3 Noodler with CVC5 matches the seven-solver portfolio while running only two tools.
AI-written summary · about
chapters (10)
- 0:00String constraints intro
- 2:29Motivation for string solvers
- 5:00String solving approaches
- 8:40Align and split for lengths
- 10:05Stabilization for regular constraints
- 11:50Stabilization + align and split
- 13:18Z3 Noodler & Mata implementation
- 14:44Performance vs state-of-the-art
- 16:32Conclusion and future work
- 17:39Q&A