Program slicing enhances a verification technique combining static and dynamic analysis

Recent research proposed efficient methods for software verification combining static and dynamic analysis, where static analysis reports possible runtime errors (some of which may be false alarms) and test generation confirms or rejects them. However, test generation may time out on real-sized programs before confirming some alarms as real bugs or rejecting some others as unreachable. To overcome this problem, we propose to reduce the source code by program slicing before test generation. This paper presents new optimized and adaptive usages of program slicing, provides underlying theoretical results and the algorithm these usages rely on. The method is implemented in a tool prototype called sante (Static ANalysis and TEsting). Our experiments show that our method with program slicing outperforms previous combinations of static and dynamic analysis. Moreover, simplifying the program makes it easier to analyze detected errors and remaining alarms.