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

摘要：

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

关键词：验证程序、循环不变式、条件赋值转换、模板、插件

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目61170070；国家科技支撑计划基金资助项目2012BAK26B01；江苏省科技支撑计划基金资助项目BE2010032

在线出版日期：2013-10-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：76-81