抽象解释为程序不变式的自动化生成提供了通用的框架。但是,该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集。因而,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确。为此,本文重点研究了抽象解释领域的相关技术。针对显式和隐式含有析取语义的循环结构,分别使用循环分解和归纳推理的方法,辅助抽象解释的分析,致力于缓解抽象解释分析中出现的语义损失问题,以提高生成的不变式的精度。本文的研究工作如下:(1)在基于语义的程序分析方面,介绍了等式转换系统的定义及其在形式化分析中的重要作用,研究了 C语言程序的等式转换系统的构造过程。介绍了最小不动点和语义格理论,阐述了不加抽象解释的等式转换系统的不可计算性。(2)在抽象解释方面,介绍了抽象解释相关的基本概念,研究了利用抽象解释框架进行程序分析的一般方法和理论。总结了抽象域的一般性构造方法,以及常用抽象域的表现形式和构造过程。针对抽象解释研究领域的三类问题:抽象解释方法本身的优化、复杂抽象域的构造和特殊程序结构的语义损失,研究了它们的产生原因和影响并且总结了现有的代表性工作。最后,研究了抽象解释在程序分析和验证领域的应用。(3)具体分析了抽象解释方法在分析含有析取语义的程序结构时的语义损失问题。针对这个问题,提出了基于循环分解和归纳推理的不变式生成改进方法,分别优化显式含有析取语义和隐式含有析取语义的程序结构的分析。该方法减少了冗余取值的带入,更贴近真实语义,从而生成更精确的不变式,并且有益于一些安全性质的推理。(4)基于上述改进方法,实现了一个自动化的不变式生成工具InvImpr,并对其进行了实验评估。实验结果表明,在时间消耗并没有增加很多的情况下,本文的改进方法相比现有同类工作能够生成更精确的不变式,对后续的程序验证和安全性质推理提供了更大的帮助。