变量极小不可满足在模型检测中的应用

• 作者: KLEINE B(U)NING Hans 王立福 陈振宇 陶志红
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 极小不可满足 抽象精化 模型检测
• 年，卷（期）: 2008,（1）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 39-47
• 页数: 9页
• 分类号: TP301
• 字数: 2974字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2008.00039

摘要

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王立福	北京大学软件与微电子学院	36	2060	16.0	36.0
2	陈振宇	东南大学计算机科学与工程学院	4	13	3.0	3.0
3	陶志红	北京大学软件与微电子学院	3	16	2.0	3.0