Enhancing symbolic execution using memoization and incremental techniques

• Main Author: Yang, Guowei, active 2013
• Format: Others
• Language: en_US
• Published: 2013
• Subjects: Symbolic execution; Incremental analysis; Trie data structure; Constraint solving; Program differencing; Assertion differencing; Software evolution
• Online Access: http://hdl.handle.net/2152/21259

The last few years have seen a resurgence of interest in the use of symbolic execution--program analysis technique developed more than three decades ago to analyze program execution paths. However, symbolic execution remains an expensive technique and scaling it remains a key technical challenge. There are two key factors that contribute to its cost: (1) the number of paths that need to be explored and (2) the cost of constraint solving, which is typically required for each path explored. Our insight is that the cost of symbolic execution can be reduced by an incremental approach, which uses static analysis and dynamic analysis to focus on relevant parts of code and reuse previous analysis results, thereby addressing both the key cost factors of symbolic execution. This dissertation presents Memoized Incremental Symbolic Execution, a novel approach that embodies our insight. Using symbolic execution in practice often requires several successive runs of the technique on largely similar underlying problems where successive problems differ due to some change, which may be to code, e.g., to fix a bug, to analysis parameters, e.g., to increase the path exploration depth, or to correctness properties, e.g., to check against stronger specifications that are written as assertions in code. Memoized Incremental Symbolic Execution, a three-fold approach, leverages the similarities in the successive problems to reduce the total cost of applying the technique. Our prototype tool-set is based on the Symbolic PathFinder. Experimental results show that Memoized Incremental Symbolic Execution enhances the efficacy of symbolic execution. === text