*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
Enabling Techniques for Symbolic Execution of Java Programs
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.
