Book chapter
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification
Computer Aided Verification, pp.453-474
Lecture Notes in Computer Science, Springer International Publishing
07/13/2017
DOI: 10.1007/978-3-319-63390-9_24
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 \documentclass[12pt]{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$$\mathsf {contains}, \mathsf {index\_of}$$\end{document} and \documentclass[12pt]{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$$\mathsf {replace}$$\end{document}. 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 \documentclass[12pt]{minimal}
\usepackage{amsmath}
\usepackage{wasysym}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{mathrsfs}
\usepackage{upgreek}
\setlength{\oddsidemargin}{-69pt}
\begin{document}$$41\% $$\end{document} of the runtime when coupled with cvc4 than when coupled with cvc4’s closest competitor while achieving comparable program coverage.
Details
- Title: Subtitle
- Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification
- Creators
- Andrew Reynolds - Department of Computer Science, The University of Iowa, Iowa City, USAMaverick Woo - CyLab, Carnegie Mellon University, Pittsburgh, USAClark Barrett - Department of Computer Science, Stanford University, Stanford, USADavid Brumley - CyLab, Carnegie Mellon University, Pittsburgh, USATianyi Liang - Two Sigma, New York, USACesare Tinelli - Department of Computer Science, The University of Iowa, Iowa City, USA
- Resource Type
- Book chapter
- Publication Details
- Computer Aided Verification, pp.453-474
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-63390-9_24
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 07/13/2017
- Academic Unit
- Computer Science
- Record Identifier
- 9984002463602771
Metrics
22 Record Views