摘要
提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效.
This paper presents a framework combining variable abstraction with bounded model checking, in order to prove the counterexamples＇ absence or establish the counterexamples＇ existence. A mathematical definition of variable minimal unsatisfiability （VMU） is introduced to drive this abstraction refinement process. The set of variables of VMU formula is a minimal one guaranteeing its unsatisfiability. Furthermore, the authors prove that VMU-driven refinement is valid and minimal by mathematical reasoning. Although the determining problem of VMU is as hard as the well-known problem called minimal unsatisfiability （MU）, i.e. De-complete, the case study has shown that VMU could be more effective than MU in variable abstraction refinement process.
出处
《软件学报》
EI
CSCD
北大核心
2008年第1期39-47,共9页
Journal of Software
基金
Supported by the National Natural Science Foundation of Chinaunder GrantNos.60425206,60773104,60403016,60633010(国家自然科学基金)
in Partby the Jiangsu Planned Projects for Postdoctoral Research Funds of Chinaunder GrantNo.0701003B(江苏省博士后科研资助计划)
关键词
极小不可满足
抽象精化
模型检测
minimal unsatisfiability
abstraction refinement
model checking
