中文摘要：

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

英文摘要：

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.