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

by Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, Cesare Tinelli
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.
Reference:
Scaling up DPLL(T) String Solvers Using Context-Dependent Simplification (Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, Cesare Tinelli), In Proceedings of the 29th International Conference on Computer Aided Verification (CAV ’17) (Rupak Majumdar, Viktor Kuncak, eds.), Springer, volume 10426, 2017. (Heidelberg, Germany)
Bibtex Entry:
@inproceedings{RWB+17,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/RWB+17.pdf",
  author    = "Andrew Reynolds and Maverick Woo and Clark Barrett and David Brumley and Tianyi Liang and Cesare Tinelli",
  title     = "Scaling up {DPLL(T)} String Solvers Using Context-Dependent Simplification",
  booktitle = "Proceedings of the 29th International Conference on Computer Aided Verification (CAV '17)",
  volume    = 10426,
  number    = 1,
  editor    = "Rupak Majumdar and Viktor Kuncak",
  pages     = "453--474",
  series    = "Lecture Notes in Computer Science",
  publisher = "Springer",
  month     = jul,
  year      = 2017,
  note      = "Heidelberg, Germany",
  category  = "Conference Publications",
  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.
"
}

Fork me on GitHub