Solver For String Constraints

Sammanfattning: Recent years have witnessed a growing number of applications that perform operationsover string data type. Reasoning over string values is crucial for the safety and securityanalyses of such applications. We present a procedure for checking the satisfiability of constraints over string data type. The procedure is designed to solve a combination of regularmembership constraints, length constraints and equality constraints. We have developeda prototypical implementation of our decision procedure and performed experimentationover a limited set of tests. The tool has exhibited inefficient performance for constraintswith relatively large number of variables or variables of large lengths. The inefficiency isdue to the exponential run time consumed in converting regular membership constraintsinto length constraints and splitting string equations into simpler equations. Alternativeapproaches for reasoning about regular membership constraints or equality constraintscould obtain better performance.