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