基于Verds的C语言子集的模型检测方法

作者：张兰兰

来源：计算机系统应用, 2013, (11): 19-25+18.

• 模型检测
• 转化
• Verds
• CEGAR
• MAGIC model checking
• tranform
• MAGIC

针对现今软件使用逻辑错误的问题越来越多的出现,提出了对最流行最普遍的编程语言——C语言子集的模型检测方法的研究.采用基于Verds工具的模型,运用C语言子集转化成Verds模型的算法,结合Verds工具和MAGIC工具实现模型检测.引入反例引导的抽象精化方法使模型检测解决状态爆炸的问题.

• 单位
  中国科学院大学; 中国科学院软件研究所; 计算机科学国家重点实验室