西安电子科技大学学报（自然科学版）2019，Vol.46Issue(1)：33-38,6.DOI:10.19665/j.issn1001-2400.2019.01.06
采用CPAChecker的动态程序验证
Dynamic program verification via a CPAChecker
摘要
Abstract
To overcome the state space explosion problem in model checking,a CPAChecker based dynamic program verification approach is proposed.The proposed approach first verifies the program statically by unwinding the control flow chart.In the process,dynamic execution is applied to accelerate the verification on the basis of the determinism of branch statements.Specifically,abstract verification effectively reduces the size of the system models,while dynamic detection not only effectively reduces false positives,but also guides the construction of more accurate system models.As a result,the proposed approach makes counterexample-guided abstraction refinement more efficient and accurate in practice.关键词
模型检测/抽象精化/动态执行/程序验证/状态空间爆炸Key words
model checking/abstract refinement/dynamic execution/program verification/state space explosion分类
信息技术与安全科学引用本文复制引用
段钊,刘锟龙..采用CPAChecker的动态程序验证[J].西安电子科技大学学报（自然科学版）,2019,46(1):33-38,6.基金项目
国家自然科学基金(61732013) （61732013）
