String Theories involving Regular Membership Predicates: From Practice to Theory and Back
This work addresses the need for efficient and reliable string solvers in formal analysis of string-heavy programs, particularly for real-world applications, and is incremental as it builds on existing benchmarks to derive theoretical insights.
The paper tackled the problem of solving string constraints in formal analysis by analyzing real-world benchmarks with regular expression predicates, proving the decidability or undecidability of extracted first-order logic theories, and found that the most common theories are PSPACE-complete, leading to a more efficient algorithm implementation.
Widespread use of string solvers in 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, especially for real-world cases. Designing an algorithm for the (generally undecidable) satisfiability problem for systems of string constraints requires a thorough understanding of the structure of constraints present in the targeted cases. In this paper, we investigate benchmarks presented in the literature containing regular expression membership predicates, extract different first order logic theories, and prove their decidability, resp. undecidability. Notably, the most common theories in real-world benchmarks are PSPACE-complete and directly lead to the implementation of a more efficient algorithm to solving string constraints.