Suzette Person's Home Page


I completed my Ph.D. in Computer Science in August 2009 and am now a Research Computer Scientist in the Formal Methods group at the NASA Langley Research Center in Hampton, VA. My current research page can be found here.

My dissertation topic is Differential Symbolic Execution (DSE)

Successful software systems tend to be long lived and evolve over time as requirements change and faults are detected. The number of times a system is updated and re-deployed may be in the hundreds, or even thousands. Re-validation of an updated system, before it is released is a critical component of the software evolution process. This step ensures that the changes made to the software have their intended effects, and that no unintended behaviors were introduced. Given the size and complexity of modern software systesm, re-validation is generally costly and time consuming. Characterizing the differences between software versions can help focus re-validation tasks, potentially reducing the cost and effort necessary to re-deploy the software. Change characterizations are also useful for other software evolution tasks, e.g., assessing the imipact of the changes on other parts of the system. Existing change characterization techniques infer differences in program behaviors based on changes to the source code. This approach is imprecise, and therefore, can lead to unnecessary effort and cause delays in deployment.

In this dissertation, we present a novel extension and application of symbolic execution techniques that computes a precise behavioral characterization of program changes. This technique, differential symbolic execution (DSE), exploits program version similarities to improve the quality of change information and reduce analysis cost. DSE is not sensitive to formatting and syntactic changes because it is based on a comparison of program semantics. It supports multiple types of equivalence checking, each of which is capable of producing a characterization of behavioral differences and similarities, expressed as sets of program inputs and their associated effects. DSE results can be used to support a wide range of software evolution tasks including program re-valiedation, impact analysis, and program documentation tasks. Its precise nature has the potential to considerably reduce software maintenance and evolution costs by enabling client analyses to use DSE results to focus on the program execution behaviors that are changed between versions.