基于SAT的软件验证

摘要：

线性时态逻辑SE-LTL是具有高表达力和基于状态、事件推理能力的并发系统规约语言.目前,SE-LTL的模型检测算法依然是显式的,状态空间爆炸是检测的主要困难.对SE-LTL引入一种有界模型检测技术,该技术将SE-LTL模型检测归约为命题公式的可满足性问题,避免了基于二叉图方法中状态空间的快速增长,加速了验证过程.对SE-LTL-X进一步在该技术中集成stuttering等价技术.实验结果表明该集成有效地降低了验证时间.

关键词： 模型检测 SAT 软件验证 形式化分析 线性时态逻辑 事件推理能力

作者: 周从华 陈振宇 鞠时光

作者单位: 江苏大学计算机科学与通信工程学院,镇江,212013 东南大学计算机科学与工程学院,南京,210096

会议类型: 国内会议

会议名称: 2007全国理论计算机科学学术年会

会议地点: 南宁

会议语种:中文

页码: 124-130

在线出版日期: 2007-11-01（万方平台首次上网日期，不代表论文的发表时间）