Saswat Anand
School of Computer Science
Georgia Institute of Technology

Committee:

Dr. Mary Jean Harrold, School of Computer Science (advisor)
Dr. Alex Orso, School of Computer Science
Dr. Santosh Pande, School of Computer Science
Dr. Willem Visser, Dept of Mathematical Sciences, Computer Science Division, University of Stellenbosch, South Africa

Abstract:

Program-analysis techniques enable software tools to reason about the behavior of software. Symbolic execution is a program-analysis technique that has been successfully used in different subfields of computer science, such as software engineering, software security and privacy, systems, and databases. The basic idea behind symbolic execution is to execute a program with symbolic values instead of actual data and compute constraints on those symbols. The constraints are then solved to generate new program inputs to explore new program behavior.

Existing symbolic execution systems for the Java programming language cannot handle large real-world programs precisely, efficiently, and automatically. Both the imprecision and the requirement of manual effort to apply symbolic execution to real-world programs arise because of (1) some features of the Java language, such as native methods and reflection that are problematic for symbolic execution, and (2) extensive use of Java’s standard library classes. Building a precise, efficient, and automatic symbolic execution system for Java requires addressing several research problems and significant system building.

The goal of this research is to address those research problems and build such a system. This goal will be achieved through the following steps. First, I will develop static analysis and program-transformation techniques that will reduce the computational cost of symbolic execution, and the imprecision and the manual effort required to apply symbolic execution on real-world programs. Next, I will implement a prototype system that will leverage the above-mentioned techniques, and to evaluate the precision, efficiency, and automation of the techniques on a set of real-world programs. Third, I will demonstrate the usefulness of symbolic execution on a set of real-world Java programs by automatically generating test-inputs for those programs using the prototype.