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

Scaling up DPLL(T) String Solvers Using Context-Dependent Simplification” by Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, and Cesare Tinelli. In Proceedings of the 29^th International Conference on Computer Aided Verification (CAV '17), (Rupak Majumdar and Viktor Kuncak, eds.), July 2017, pp. 453-474. Heidelberg, Germany.


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.

BibTeX entry:

   author = {Andrew Reynolds and Maverick Woo and Clark Barrett and David
	Brumley and Tianyi Liang and Cesare Tinelli},
   editor = {Rupak Majumdar and Viktor Kuncak},
   title = {Scaling up {DPLL(T)} String Solvers Using Context-Dependent
   booktitle = {Proceedings of the {\it 29^{th}} International Conference
	on Computer Aided Verification (CAV '17)},
   series = {Lecture Notes in Computer Science},
   volume = {10426},
   number = {1},
   pages = {453--474},
   publisher = {Springer},
   month = jul,
   year = {2017},
   note = {Heidelberg, Germany},
   url = {}

(This webpage was created with bibtex2web.)