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

An Adaptive Loop Invariant Generation Approach

作　　者：刘自恒[1] 曾庆凯[1,2] 

机构地区：[1]南京大学计算机科学与技术系,210093 [2]南京大学计算机软件新技术国家重点实验室,210093

出　　处：《计算机工程》2013年第6期76-81,共6页Computer Engineering

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

摘　　要：基于条件赋值转换和自适应模板生成技术,提出一种自适应的的循环不变式生成方法。该方法在生成过程中综合考虑函数规范、循环本身、循环后操作等信息,有针对性地发现潜在的循环不变式,并在Frama-C平台上实现一个插件loopInv。实验结果表明,与invGen和gin-pink工具相比,loopInv的应用更加有效,可较好地完成多数程序的验证过程。This paper proposes an improved approach to infer loop invariants which is based on conditional assignment conversion and adaptive template. Many semantic factors are considered during the generation which makes it more automatic and adaptive. A plugin named looplnv is designed and implemented. Experimental results show that the analysis is more effective, compared with other selected tools, such as invGen and gin-pink, which makes most of the procedures verified successfully.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]