Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification

Posted ON July 22, 2017

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.

DOI: 10.1007/978-319-63390-9_24

Related Articles

Life at Two Sigma

We’re rigorous about our work and developing our people.

Learn More

Interested in working at Two Sigma? Explore careers.

This website uses cookies to ensure you get the best experience on our website. Learn More
Got It