有界模型检测的优化

• 作者: 杨晋吉 林瀚 肖茵茵 苏开乐 骆翔宇
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型检测 有界模型检测 可满足性问题 模态算子 递推公式
• 年，卷（期）: 2009,（8）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 2005-2014
• 页数: 10页
• 分类号: TP301
• 字数: 9517字
• 语种: 中文

摘要

公式的逻辑关系.通过实验比较分析,在生成SAT实例规模和易求解方面都优于BMC中求解这些模态算子的现有的两种重要方法AA_BMC和Timo_BMC.所给出的方法和思想对于BMC中验证其他模态算子时的编码优化也有参考价值.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	肖茵茵	中山大学信息科学与技术学院	11	57	5.0	7.0
2	苏开乐	北京大学信息科学技术学院	8	82	5.0	8.0
3	杨晋吉	华南师范大学计算机学院	10	111	6.0	10.0
5	林瀚	中山大学信息科学与技术学院	5	41	2.0	5.0
8	骆翔宇	桂林电子科技大学计算机与控制学院	13	65	5.0	7.0