Abstract: In view of suffering the problem of high false alarms rate, a false alarm reducing method based on weakest precondition propagation for static analysis is proposed. According to different software security property, the weakest precondition at the beginning of the procedure can be obtained from the target state in a demand-driven way. False alarms will be reduced by determining the satisfiability of the precondition formulae. The approach is instantiated to reduce false alarms for static detection of array bounds violation and null pointer dereference. The experiments show that the technique is successful and suitable for reducing false alarms for static analysis.

Key words: static analysis, reduce false alarms, weakest precondition, array bounds violation, null pointer dereference

摘要： 针对程序静态分析技术误报过多的问题，提出一种基于最弱前置条件的静态分析误报消除方法。根据不同的软件安全性质，从目标状态出发，以需求驱动的方式得到过程起始位置的最弱前置条件，判断该条件公式的可满足性来消除误报。将该方法实例化来消除静态分析工具检测数组访问越界和空指针解引用的误报，实验结果表明该方法是有效且实用的。

关键词: 静态分析, 误报消除, 最弱前置条件, 数组访问越界, 空指针解引用