Locality-guided based optimization method for bounded model checker - Shun WANG; Ye DU; Zhen HAN; Jiqiang LIU (Tongxin xuebao)
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 programming pattern or learned through verifying procedure to help eliminate the redundant state has been proved effective.Definition 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 software modules.