For software model checking, approaches that combine with different kind of verification methods are now under research. The key to improve scale and complexity of verifiable software is handling the method for abstraction widening and strengthening wisely and precisely. To archive that, using extra knowledge that extracted from program-ming pattern or learned through verifying procedure to help eliminate the redundant state has been proved effective. Def-inition of program locality was given. It took the important role in accelerating software verification, then the strategy was raised and an algorithm was implemented to take advantage of program locality. This method exploits the features of modern BMC (bounded model checker) and scales up the capability of its power in large scale and comprehensive soft-ware modules.%基于多种模型检测方法组合的复合检测方式是当前软件模型检测领域开展研究的热点之一.在当前的研究中,提高检测的规模和检测的对象复杂程度的关键在于如何有效处理抽象的扩张和收缩.证明通过对程序模式或验证信息的利用可以加快状态空间的探索速度.面向有界模型检测(BMC)加速方法展开研究,使用程序中额外的信息和知识对其处理以协助检测器删除冗余和无效的状态.在对程序局部性进行定义的基础上,对其加速性进行讨论,提出一种加速有界检测的方法和一种改进策略,对算法进行了详细描述,并通过实验验证了方法在检测效率和性能上的优越性.
展开▼
