2021/05/15 by Murphy Berzish, Joel D. Day, Berzish, Murphy +11
Computer Science · Social Sciences · #Access Control and Trust #Computation and Language (cs.CL) #FOS: Computer and information sciences #Software Testing and Debugging Techniques #Web Application Security Vulnerabilities
paper · pdf · doi:10.48550/arxiv.2105.07220
openalex publication_date 2021/05/15 · openalex created_date 2022/09/17 · openalex updated_date 2026/07/28
Widespread use of string solvers in formal analysis of string-heavy programs\nhas led to a growing demand for more efficient and reliable techniques which\ncan be applied in this context, especially for real-world cases. Designing an\nalgorithm for the (generally undecidable) satisfiability problem for systems of\nstring constraints requires a thorough understanding of the structure of\nconstraints present in the targeted cases. In this paper, we investigate\nbenchmarks presented in the literature containing regular expression membership\npredicates, extract different first order logic theories, and prove their\ndecidability, resp. undecidability. Notably, the most common theories in\nreal-world benchmarks are PSPACE-complete and directly lead to the\nimplementation of a more efficient algorithm to solving string constraints.\n