一种自适应的循环不变式生成方法

• 作者: 刘自恒 曾庆凯
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 验证程序 循环不变式 条件赋值转换 模板 插件
• 年，卷（期）: 2013,（6）
• 所属期刊栏目: 体系结构与软件技术
• 页码范围: 76-81
• 页数: 6页
• 分类号: TP311
• 字数: 6566字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2013.06.015

摘要

基于条件赋值转换和自适应模板生成技术，提出一种自适应的的循环不变式生成方法。该方法在生成过程中综合考虑函数规范、循环本身、循环后操作等信息，有针对性地发现潜在的循环不变式，并在Frama-C平台上实现一个插件loopInv。实验结果表明，与invGen和gin-pink工具相比，loopInv的应用更加有效，可较好地完成多数程序的验证过程。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	曾庆凯	南京大学计算机科学与技术系	58	555	13.0	21.0
5	刘自恒	南京大学计算机科学与技术系	1	2	1.0	1.0