-
题名基于CEGAR偏序化简的并行程序死锁检测
被引量：3
- 1
-
-
作者
梁中兴
罗贵明
旷宏斌
-
机构
清华大学软件学院
-
出处
《计算机工程》
CAS
CSCD
北大核心
2009年第19期65-68,共4页
-
基金
国家自然科学基金资助项目(60672110
60635020)
-
文摘
针对并发程序的模型检测存在大量的冗余交互和严重的状态空间爆炸问题,提出以迁移标记系统为建模语言计算Persistent Set并完成偏序化简的算法。将算法和CEGAR算法结合起来,实现对并发C程序的并行死锁检测。结果证明该算法在减缓状态空间爆炸和模型验证的效率方面较以往的算法有所提高。
-
关键词
模型检测
cegar算法
偏序化简
-
Keywords
model eheking
Counterexample-Guided Abstraction Refinement（cegar） algorithm
partial-order reduction
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名一种C程序断言的全自动静态验证方法
被引量：1
- 2
-
-
作者
易晓东
杨学军
-
机构
国防科技大学计算机学院
-
出处
《计算机科学》
CSCD
北大核心
2006年第9期253-256,273,共5页
-
基金
863重大软件专项No.2002AA1Z2101~~
-
文摘
在软件程序中插入断言是保证软件质量的一个简单但有效的方法,人们常使用测试的方法检验程序中的断言是否满足,但测试很难保证验证的完备性。本文提出了一种可以保证完备性的全自动静态断言验证方法,其基本思想是基于程序切片符号执行程序的所有执行路径,并证明路径上的所有断言都满足。为了尽量减少符号执行的语句的数量,使用了基于反例的抽象精化方法,从一个粗略的切片标准开始迭代地符号执行一条路径,根据验证的反例自动生成下一次迭代过程中使用的精化的切片标准。包含循环的程序可能具有无穷多条程序执行路径,提出的基于符号执行上下文不变式证明的方法可以证明由于循环导致的无穷多条路径中断言都满足,从而使得验证过程可以终止。实验表明,提出的全自动静态断言验证方法不仅可行,而且验证代价较小,具有较强的实用性。
-
关键词
断言验证
基于程序切片的符号执行
基于反例的抽象精化
静态分析
-
Keywords
Assertion verification,Symbolic execution based on program slicing, cegar, Static analysis
-
分类号
TP391.9
[自动化与计算机技术—计算机应用技术]
-
-
题名基于Verds的C语言子集的模型检测方法
- 3
-
-
作者
张兰兰
-
机构
中国科学院软件研究所计算机科学国家重点实验室
中国科学院大学
-
出处
《计算机系统应用》
2013年第11期19-25,18,共8页
-
基金
国家科技重大专项(2012ZX01039-004)
-
文摘
针对现今软件使用逻辑错误的问题越来越多的出现,提出了对最流行最普遍的编程语言——C语言子集的模型检测方法的研究.采用基于Verds工具的模型,运用C语言子集转化成Verds模型的算法,结合Verds工具和MAGIC工具实现模型检测.引入反例引导的抽象精化方法使模型检测解决状态爆炸的问题.
-
关键词
模型检测
转化
Verds
cegar
MAGIC
-
Keywords
model checking
tranform
Verds
cegar
MAGIC
-
分类号
TP311.52
[自动化与计算机技术—计算机软件与理论]
-
-
题名VASR-CBMC:基于变量子图的多线程程序验证
- 4
-
-
作者
李运筹
尹平
尹良泽
-
机构
北京跟踪与通信技术研究所
国防科技大学计算机学院
-
出处
《计算机应用研究》
CSCD
北大核心
2018年第8期2393-2396,共4页
-
文摘
Yogar-CBMC基于事件顺序图实现了反例抽象精化思想,是当前最有效的多线程程序验证工具之一。针对事件顺序图过于复杂,导致判断反例可行性及求解精化约束耗时过长的问题,提出变量子图概念及基于变量子图的抽象精化方法,将全局事件顺序图分解为连通等价的变量子图集,基于变量子图执行反例验证与精化求解,从而有效缩小图的规模,提升验证效率。将该方法实现为VSAR-CBMC,实验证明其相较于Yogar-CBMC验证时间平均缩短43%,有效提升了模型检验对并发程序的验证能力。
-
关键词
程序验证
变量子图
反例抽象精化
事件顺序图
-
Keywords
program verification
variable subgraph
cegar
event order graph
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-
