Paper Info
Title
Z3str2: an efficient solver for strings, regular expressions, and length constraints.
Abstract
In recent years, string solvers have become an essential component in many formal verification, security analysis, and bug-finding tools. Such solvers typically support a theory of string equations, the length function, and the regular-expression membership predicate. These enable considerable expressive power, which comes at the cost of slow solving time, and in some cases even non-termination. We present three techniques, designed for word-based SMT string solvers, to mitigate these problems: (1) detecting overlapping variables, which is essential to avoiding common cases of non-termination; (2) pruning of the search space via bi-directional integration between the string and integer theories, enabling new cross-domain heuristics; and (3) a binary search based heuristic, allowing the procedure to skip unnecessary string length queries and converge on consistent length assignments faster for large strings. We have implemented above techniques atop the Z3-str solver, resulting in a significantly more robust and efficient solver, dubbed Z3str2, for the quantifier-free theory of string equations, the regular-expression membership predicate, and linear arithmetic over the length function. We report on a series of experiments over four sets of challenging real-world benchmarks, where we compare Z3str2 with five different string solvers: S3, CVC4, Kaluza, PISA and Stranger. Each of these tools utilizes a different solving strategy and/or string representation (based e.g. on words, bit vectors or automata). The results point to the efficacy of our proposed techniques, which yield dramatic performance improvement. We also demonstrate performance improvements enabled by Z3str2 in the context of symbolic execution for string-manipulating programs. We observe that the techniques presented here are of broad applicability, and can be integrated into other string solvers to improve their performance.
Year
DOI
Venue
2017
10.1007/s10703-016-0263-6
Formal Methods in System Design
Keywords
Field
DocType
String constraint solver,SMT solver,String analysis
String searching algorithm,Regular expression,Commentz-Walter algorithm,Computer science,Algorithm,Theoretical computer science,Symbolic execution,Solver,String metric,String (computer science),Boyer–Moore string search algorithm
Journal
Volume
Issue
ISSN
50
2-3
0925-9856
Citations 
PageRank 
References 
3
0.41
29
Authors
7
Name
Order
Citations
PageRank
Yunhui Zheng130118.09
Vijay Ganesh2156394.66
Sanu Subramanian330.41
Omer Tripp449226.38
Murphy Berzish5102.59
Julian Dolby6138974.44
Xiangyu Zhang72857151.00