有界模型检验综述
无论是计算机系统硬件设计还是软件设计,随着设计规模越来越复杂和庞大,会产生越来越多的设计缺陷.传统检测方法代价高,并且难以检测这些设计缺陷.有界模型检验是一种重要的形式化验证方法,可以大大提高检测、验证的效率.作为一种形式化方法构造系统的模拟运行过程,有界模型检验通过把有限状态机和线性时序逻辑验证规范否定形式编码成布尔可满足性实例,再由各种布尔可满足性工具来求解,以获得反例.由于有界模型检验使用深度优先搜索,它可以很快找到路径最短的反例.
有界模型检验、模型检验、SAT
13
TP311(计算技术、计算机技术)
2018-01-12（万方平台首次上网日期，不代表论文的发表时间）
共2页
70-71
