摘要
基于条件赋值转换和自适应模板生成技术,提出一种自适应的的循环不变式生成方法。该方法在生成过程中综合考虑函数规范、循环本身、循环后操作等信息,有针对性地发现潜在的循环不变式,并在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.
出处
《计算机工程》
CAS
CSCD
2013年第6期76-81,共6页
Computer Engineering
基金
国家自然科学基金资助项目(61170070)
国家科技支撑计划基金资助项目(2012BAK26B01)
江苏省科技支撑计划基金资助项目(BE2010032)
关键词
验证程序
循环不变式
条件赋值转换
模板
插件
verification procedures
loop invariant
conditional assignment conversion
template
plugin