中文摘要：

介绍了推广化符号轨迹赋值中常用的模型检验强可满足性算法,分析了产生伪报错的原因,提出了一种降低伪报错的改进算法.该算法在前算法的基础之上减少了边的计算量,降低了由于抽象带来的伪报错问题,从而大大提高了计算过程中的准确率.实验结果表明,该改进算法在降低伪报错和减少计算量方面有明显提高.

英文摘要：

The paper introduced a strong model checking （SMC） algorithm in generalized symbolic trajectory evaluation （GSTE） and analyzed the reason leading to false negative, proposed the improved SMC algorithm to reduce the false negative. The algorithm decreases the calculation on the edges and takes the false negative from abstract to improve the accuracy. Experimental results show the improved algorithm makes a big progress on reducing false negative and calculation.