基于CEGAR偏序化简的并行程序死锁检测

• 作者: 旷宏斌 梁中兴 罗贵明
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 模型检测 CEGAR算法 偏序化简
• 年，卷（期）: 2009,（19）
• 所属期刊栏目: 软件技术与数据库
• 页码范围: 65-68
• 页数: 4页
• 分类号: TP311
• 字数: 7033字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2009.19.021

摘要

针对并发程序的模型检测存在大量的冗余交互和严重的状态空间爆炸问题,提出以迁移标记系统为建模语言计算Persistent Set并完成偏序化简的算法.将算法和CEGAR算法结合起来,实现对并发C程序的并行死锁检测.结果证明该算法在减缓状态空间爆炸和模型验证的效率方面较以往的算法有所提高.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	罗贵明	清华大学软件学院	19	125	6.0	10.0
2	梁中兴	清华大学软件学院	1	5	1.0	1.0
3	旷宏斌	清华大学软件学院	1	5	1.0	1.0