关键词: 静态分析, 速度重比重静态分析工具, 层次式分析, 警告程序切片, SAT求解器

Abstract: To increase the accuracy and credibility of outputs for static analysis tool of speed heavy proportion, this paper proposes a hierarchical static testing method. In the first level, the static analysis tool of speed heavy proportion is selected to generate the initial outputs of detection. In the second level, the alarm messages of the initial test results are used to extract the program slices. The alarm program slices are formally abstracted into Boolean formula to determine the true-false of slices by the SAT solver. The accuracy of analysis tools is improved by integrating the results of the first level and the second level. The experimental results show that the method can improve the accuracy and credibility of analysis tools in a certainty and can also reduce the false positives effectively.

Key words: static analysis, static analysis tool of speed heavy proportion, hierarchical analysis, alarm program slice, SAT solver