| 本文已被：浏览 5799次 下载 6571次 |
码上扫一扫！ |
|
|
| 变量极小不可满足在模型检测中的应用 |
|
陈振宇1, 陶志红2, KLEINE BüNING Hans3, 王立福2
|
|
1.东南大学 计算机科学与工程学院,江苏 南京 210096;2.北京大学 软件与微电子学院,北京 100871;3.Department of Computer Science, University of Paderborn, Paderborn 33095, Germany
|
|
| 摘要: |
| 提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效. |
| 关键词: 极小不可满足 抽象精化 模型检测 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60425206, 60773104, 60403016, 60633010 (国家自然科学基金); in Part by the Jiangsu Planned Projects for Postdoctoral Research Funds of China under Grant No.0701003B (江苏省博士后科研资助计划) |
|
| Applying Variable Minimal Unsatisfiability in Model Checking |
|
CHEN Zhen-Yu,TAO Zhi-Hong,KLEINE BüNING Hans,WANG Li-Fu
|
| Abstract: |
| 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. DP-complete, the case study has shown that VMU could be more effective than MU in variable abstraction refinement process. |
| Key words: minimal unsatisfiability abstraction refinement model checking |
