Strategies for scalable symbolic execution-driven test generation for programs  

作　　者：KRISHNAMOORTHY Saparya HSIAO Michael S. LINGAPPAN Loganathan 

机构地区：[1]Intel Corporation [2]Department of Electrical and Computer Engineering,Virginia Polytechnic Institute and State University

出　　处：《Science China(Information Sciences)》2011年第9期1797-1812,共16页中国科学（信息科学）（英文版）

基　　金：supported in part by a grant from Intel Corporation

摘　　要：With the advent of advanced program analysis and constraint solving techniques, several test generation tools use variants of symbolic execution. Symbolic techniques have been shown to be very effective in path-based test generation; however, they fail to scale to large programs due to the exponential number of paths to be explored. In this paper, we focus on tackling this path explosion problem and propose search strategies to achieve quick branch coverage under symbolic execution, while exploring only a fraction of paths in the program. We present a reachability-guided strategy that makes use of the reachability graph of the program to explore unvisited portions of the program and a conflict-driven backtracking strategy that utilizes conflict analysis to perform nonchronological backtracking. We present experimental evidence that these strategies can significantly reduce the search space and improve the speed of test generation for programs.With the advent of advanced program analysis and constraint solving techniques, several test generation tools use variants of symbolic execution. Symbolic techniques have been shown to be very effective in path-based test generation; however, they fail to scale to large programs due to the exponential number of paths to be explored. In this paper, we focus on tackling this path explosion problem and propose search strategies to achieve quick branch coverage under symbolic execution, while exploring only a fraction of paths in the program. We present a reachability-guided strategy that makes use of the reachability graph of the program to explore unvisited portions of the program and a conflict-driven backtracking strategy that utilizes conflict analysis to perform nonchronological backtracking. We present experimental evidence that these strategies can significantly reduce the search space and improve the speed of test generation for programs.

关 键 词：test generation software testing symbolic execution path explosion conflict analysis 

分 类 号：TP311.53[自动化与计算机技术—计算机软件与理论]