Loop Extended Symbolic Execution on List Manipulating Programs
Current symbolic execution is challenged by its ability to deal with loops. The case gets worse for loops manipulating recursive data structures. In this paper, we extend classic symbolic execution techniques for error detection of programs manipulating lists in loops. The idea is to enhance the symbolic execution with the utilization of quantitative aspect of the shape, and to construct the exit state of the loop. The exit state is constrained by a set of numeric constraints containing normal symbolic variables in programs and instrumented symbolic variables on the shapes. A prototype tool has been implemented and experiments are conducted on some commonly used list manipulating programs.
symbolic execution list manipulating programs loop handling
Renjian Li Zhaofei Wang Longming Dong
National Laboratory for Parallel and Distributed Processing,National University of Defense Technology 410073, Changsha, China
国际会议
合肥
英文
3010-3014
2011-09-23（万方平台首次上网日期，不代表论文的发表时间）