%0 Journal Article
%T 一种基于满足性判定的并发软件验证策略
%A 周从华？
%J 软件学报
%P 1414-1424
%D 2009
%X 对线性时态逻辑se-ltl提出了一种基于sat的有界模型检测过程,该过程避免了基于bdd方法中状态空间快速增长的问题.在se-ltl的子集se-ltl?x的有界模型检测过程中,集成了stuttering等价技术,该集成有效地加速了验证过程.进一步提出了一种组合了基于sat的有界模型检测、基于反例的抽象求精、组合推理3种状态空间约简技术的并发软件验证策略.该策略中,抽象和求精在每一个构件上独立进行.同时,模型检测的过程是符号化的.实例表明,该策略降低了验证时间和对内存空间的需求.
%K 有界模型检测
%K 抽象
%K 平行组合
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=558&flag=1