SPA: Symbolic Program Approximation for Scalable Path-sensitive Analysis

Symbolic execution is a static-analysis technique that has been used \nfor applications such as test-input generation and change analysis. \nSymbolic execution’s path sensitivity makes scaling it difficult. \nDespite recent advances that reduce the number of paths to \nexplore, the scalability problem remains. Moreover, there are applications \nthat require the analysis of all paths in a program fragment, \nwhich exacerbate the scalability problem. In this paper, we \npresent a new technique, called Symbolic Program Approximation \n(SPA), that performs an approximation of the symbolic execution \nof all paths between two program points by abstracting away certain \nsymbolic subterms to make the symbolic analysis practical, at \nthe cost of some precision. We discuss several applications of SPA, \nincluding testing of software changes and static invariant discovery. \nWe also present a tool that implements SPA and an empirical evaluation \non change analysis and testing that shows the applicability, \neffectiveness, and potential of our technique.