272 / 1971-01-01 00:00:00

Symbolic Execution Based On Context-sensitive, Path-sensitive Slicing And Refactoring

5735

Symbolic execution is a systematic program analysis technique that has become increasingly popular in network software testing, due to algorithmic advances and availability of computational power and constraint solving technology. Recent research utilizes symbolic execution to verify alarms that static analysis reports. However, A main challenge is to detect determining symbolic values for program variables related to library and combination explosion of loop paths. Test generation may time out on real-sized programs before confirming some alarms as real bugs or rejecting some others as unreachable. In this paper, we propose a symbolic analysis based on context-sensitive, path-sensitive slicing and refactoring, a hybrid technique that enables fully automatic symbolic analysis even for the traditionally challenging code. The novelties of this work are threefold: 1) new optimized and adaptive usages of context-sensitive and path-sensitive slicing to reduce the program’s complexity 2) refactoring sliced program with the loop and library model and 3) dynamic executions are performed on the refactored program. Our method is implemented in SESR framework. Our experiments show that our method with program slicing outperforms previous symbolic execution. Moreover, simplifying the program makes it easier to analyze detected errors and remaining alarms.