欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
提出一个结合变量抽象和有界模型检测（BMC）的验证框架，用于证明反例不存在或输出存在反例，引入变量极小不可满足（VMU）的数学概念来驱动抽象精化的验证过程，一个VMU公式F的变量集合是保证其不可满足性的一个极小集合．严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质：有效性和极小性．虽然VMU的判定问题和极小不可满足（MU）一样难，即D^p完全的，该案例研究表明，在变量抽象精化过程中，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.
同期刊论文项目
同项目期刊论文
An XML query rewriting mechanism with multiple ontologies integration based on complex semantic mapp
期刊信息
位置：