Title: Differential Symbolic Execution

Abstract:
Detecting and characterizing the effects of software changes is a fundamental component of software maintenance. Version differencing information can be used to perform version merging, infer change characteristics, produce program documntation, and guide program re-validation. Existing techniques for characterizing code changes, however, are imprecise leading to unnecessary maintenance efforts.

In this work, we introduce a novel extension and application of symbolic execution techniques that computes a precise behavioural characterization of a program change. This technique, which we call differential symbolic execution (DSE), exploits the fact that program versions are largely similar to reduce cost and improve the quality of analysis results. We define the foundational concepts of DSE, describe cost-effective tool support for DSE, and illustrate its potential benefit through an exploratory study that considers version histories of two Java code bases.