The Theory and Practice of String Solvers (Invited Talk Abstract)
The paper titled “Hampi: A Solver for String Constraints” was published in the proceedings of the International Symposium on Software Testing and Analysis (ISSTA) 2009, and has been selected to receive the ISSTA 2019 Impact Paper Award. The paper describes HAMPI, a system for solving the satisfiability problem for a rich theory of string (word) equations, operations over strings, and predicates over regular expressions and context-free grammars. HAMPI was one of the first practical string solvers aimed at software engineering and security problems, and has inspired considerable research on string solving algorithms and their applications. We review the work on the theory and practice of string solving algorithms over the last decade, specifically highlighting key historical developments that have led to their widespread use. On the practical front, we discuss different kinds of algorithmic paradigms, such as word- and automata-based, that have been developed to solve string and regular expression constraints. We then focus on the many hardness results that theorists have proved for fragments of theories over strings. Finally, we conclude with open theoretical problems, practical algorithmic challenges, and future applications of string solvers especially for security of web applications.