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

Download PDF — 618.52 KB

The final publication is available at Springer via https://doi.org/10.1007/978-3-319-63390-9_24

The views expressed above are not necessarily the views of Two Sigma Investments, LP or any of its affiliates (collectively, “Two Sigma”).  The information presented above is only for informational and educational purposes and is not an offer to sell or the solicitation of an offer to buy any securities or other instruments. Additionally, the above information is not intended to provide, and should not be relied upon for investment, accounting, legal or tax advice. Two Sigma makes no representations, express or implied, regarding the accuracy or completeness of this information, and the reader accepts all risks in relying on the above information for any purpose whatsoever. Click here for other important disclaimers and disclosures.