Abstraction of symbolic execution for 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. This thesis demonstrates the ability to symbolically execute the Java string classes, at an abstract level. Using finite-state automata to represent details of the string manipulation, the implementation allows symbolic execution to scale to more complex programs. This technique can be applied to programs which generate complicated strings, such as SQL database queries. Test results from a variety of programs that make extensive use of strings demonstrate the effectiveness of the implementation.Electrical and Computer Engineerin