软件作为信息系统的实现载体,广泛应用在各个领域,软件中的任何安全漏洞或错误的实现都可能导致非常严重的后果。通过大量的测试可以提高软件的可靠性,但成本较高,也不能完全保证软件的可靠。形式化证明方法基于严密的数学和逻辑基础,经过正确性证明的程序可以保证软件符合指定的程序规范,从而大大提高软件可靠性。程序正确性证明的一个关键问题是发现充分的循环不变式信息来辅助、支撑证明过程的完成。由人工寻找循环不变式工作繁琐,容易出错。因此,研究如何自动地有效分析和生成循环不变式,使得软件证明过程顺利完成,成为形式化方法研究领域的一个重要研究课题。本文主要针对软件验证技术中的循环不变式生成技术进行研究和实现：(1)对形式化程序分析方法主要理论进行总结。本文根据形式化分析中用到的主要理论的不同对形式化分析技术进行总结。对各自的理论核心、主要解决的问题、典型工具进行了阐述。在此基础上,指出形式化证明过程的难点,并总结了当前克服这些难点所采用的方法。(2)介绍和总结了目前求解循环不变式的主要研究状况和现有方法。根据他们主要理论和适用范围的不同进行阐述,指出了目前工作存在的不足。(3)本文提出了一种基于条件赋值转换和自适应模板技术的循环不变式生成方法。根据程序控制流结构、依赖分析结果和值分析结果,生成可能的循环不变式,然后由定理证明器求解。该方法可以自动地运行,并将结果以ACSL注释的形式添加到程序中,辅助完成程序属性的证明过程。(4)基于上述方法,在Frama-C平台和APRON库的基础上,实现了一个分析插件loopInv。选取了一些程序作为分析对象,与其他方法作了比较,结果表明可以发现更多的不变式,使一些程序规范顺利得到证明。