通信学报2018，Vol.39Issue(3)：181-190,10.DOI:10.11959/j.issn.1000-436x.2018050
基于程序局部性引导的有界模型检测优化方法
Locality-guided based optimization method for bounded model checker
摘要
Abstract
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/软件检测/局部性/优化Key words
model checking/BMC/software verification/locality/optimization分类
信息技术与安全科学引用本文复制引用
王舜,杜晔,韩臻,刘吉强..基于程序局部性引导的有界模型检测优化方法[J].通信学报,2018,39(3):181-190,10.基金项目
北京高校青年英才计划基金资助项目(No.YETP0548) （No.YETP0548）
国家自然科学基金资助项目(No.61672092)Beijing Higher Education Young Elite Teacher Project (No.YETP0548), The National Natural Science Founda-tion of China (No.61672092) （No.61672092）
