"Solving String Constraints with Lengths by Stabilization"

[github-actions]

"This paper was randomly selected as your next reading.\n\n###Solving String Constraints with Lengths by Stabilization\n\nWe present a new algorithm for solving string constraints. The algorithm builds upon a recent method for solving word equations and regular constraints that interprets string variables as languages rather than strings and, consequently, mitigates the combinatorial explosion that plagues other approaches. We extend the approach to handle linear integer arithmetic length constraints by combination with a known principle of equation alignment and splitting, and by extension to other common types of string constraints, yielding a fullyfledged string solver. The ability of the framework to handle unrestricted disequalities even extends one of the largest decidable classes of string constraints, the chainfree fragment. We integrate our algorithm into a DPLLbased SMT solver. The performance of our implementation is competitive and even significantly better than stateoftheart string solvers on several established benchmarks obtained from applications in verification of string programs.\n\nChen, YuFang, et al. “Solving String Constraints with Lengths by Stabilization. Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023, pp. 211241. Crossref, https://doi.org/10.1145/3622872.\n\nMerge this PR to apply selection."