Evaluation of string constraint solvers in the context of Symbolic execution

Symbolic execution tools query constraint solvers for tasks such as determining the feasibility of program paths. Therefore, the effectiveness of such tools depends on their constraint solvers. Most modern constraint solvers for primitive types are efficient and accurate. However, research on constraint solvers for complex types, such as strings, is less converged. In this paper, we introduce two new solver adequacy criteria, modeling cost and accuracy, to help the user identify an adequate solver. Using these metrics and performance criterion, we evaluate four distinct string constraint solvers in the context of symbolic execution. Our results show that, depending on the needs of the user and composition of the program, one solver might be more appropriate than another. Yet, none of the solvers exhibit the best results for all programs. Hence, if resources permit, the user will benefit the most from executing all solvers in parallel and enabling communication between solvers.