基于SAT的软件验证

扫码查看

原文链接

NETL

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

作者：

周从华、陈振宇、鞠时光

展开 >

作者单位：

江苏大学计算机科学与通信工程学院,镇江,212013

东南大学计算机科学与工程学院,南京,210096

关键词：

模型检测 SAT 软件验证形式化分析

主办单位：

中国计算机学会

广西大学

计算机研究与发展编辑部

会议名称：

2007全国理论计算机科学学术年会

会议时间：

2007-11-01

会议地点：

南宁

会议母体文献：

2007全国理论计算机科学学术年会论文集

页码：

124-130

出版时间：

2007