SPA: Symbolic Program Approximation for Scalable Path-sensitive Analysis

Show full item record

Please use this identifier to cite or link to this item:

Title: SPA: Symbolic Program Approximation for Scalable Path-sensitive Analysis
Author: Harrold, Mary Jean ; Santelices, Raul
Abstract: Symbolic execution is a static-analysis technique that has been used for applications such as test-input generation and change analysis. Symbolic execution’s path sensitivity makes scaling it difficult. Despite recent advances that reduce the number of paths to explore, the scalability problem remains. Moreover, there are applications that require the analysis of all paths in a program fragment, which exacerbate the scalability problem. In this paper, we present a new technique, called Symbolic Program Approximation (SPA), that performs an approximation of the symbolic execution of all paths between two program points by abstracting away certain symbolic subterms to make the symbolic analysis practical, at the cost of some precision. We discuss several applications of SPA, including testing of software changes and static invariant discovery. We also present a tool that implements SPA and an empirical evaluation on change analysis and testing that shows the applicability, effectiveness, and potential of our technique.
Type: Technical Report
Date: 2009
Contributor: Georgia Institute of Technology. College of Computing
Georgia Institute of Technology. Center for Experimental Research in Computer Systems
Relation: CERCS ; GIT-CERCS-09-08
Publisher: Georgia Institute of Technology
Subject: Backward expansion
Dependence analysis
Dependence chain
Symbolic execution
Symbolic Program Approximation (SPA)

All materials in SMARTech are protected under U.S. Copyright Law and all rights are reserved, unless otherwise specifically indicated on or in the materials.

Files in this item

Files Size Format View
git-cercs-09-08.pdf 206.7Kb PDF View/ Open

This item appears in the following Collection(s)

Show full item record