Abstracting Symbolic Execution with String Analysis

Forward symbolic execution is a technique for program analysis that explores the execution paths of a program by maintaining a symbolic representation of the program state. Traditionally, applications of this technique have focused on symbolically representing only primitive data types, while more recent extensions have expanded to reference types. We demonstrate the ability to symbolically execute a commonly used library class, specifically a string, at an abstract level. By abstracting away the implementation details of strings using finite-state automata, symbolic execution can scale to more complex programs. This technique can be applied to programs which generate complicated strings, such as SQL database queries.