Quantification of Software Changes through Probabilistic Symbolic Execution

Characterizing software changes is a fundamental component of software maintenance. Despite being widely used and computationally efficient, techniques that characterize syntactic program changes lack an insight on the changed program behaviors and can possibly lead to unnecessary maintenance efforts. Recent promising techniques use program analysis to produce a behavioral characterization of program changes, see e.g. [10, 12]. Behaviors are either abstracted through operational models (e.g., transition systems) or summarized through a set of logical formulae satisfied by the input-output relation (e.g., pre- and post- conditions). Checking the implication or the equivalence between the abstraction of different program versions provides a qualitative assessment of the preservation of desired behaviors or the elimination of undesired behaviors. Nonetheless, such qualitative assessment provides only true-false answers, providing limited guid-ance on “how far ” two versions are different from one another. Recent work [8, 9] provides more informative but still only qualitative representation of the difference. We argue that a com-plementary quantitative representation for software changes is needed, particularly for programs required to operate under uncertainty usage profiles, where the goal of maintenance is to improv