Authors: Tianyi Liang (Two Sigma), Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Cesare Tinelli
Publication venue: 29th International Conference on Computer Aided Verification (CAV 2017), Heidelberg, Germany
Abstract: Efficient reasoning about strings is essential to a growing number of security and verification applications. We describe satisfiability checking techniques in an extended theory of strings that includes operators commonly occurring in these applications, such as contains, index_of and replace. We introduce a novel context-dependent simplification technique that improves the scalability of string solvers on challenging constraints coming from real-world problems. Our evaluation shows that an implementation of these techniques in the SMT solver CVC4 significantly outperforms state-of-the-art string solvers on benchmarks generated using PyEx, a symbolic execution engine for Python programs. Using a test suite sampled from four popular Python packages, we show that PyEx uses only 41% of the runtime when coupled with CVC4 than when coupled with CVC4’s closest competitor while achieving comparable program coverage.
