随着软件需求的不断增加,软件系统日趋复杂与庞大,软件的可信性要求越来越高,尤其是在航空、航天、医疗、金融等安全攸关领域。许多安全攸关软件特别是嵌入式软件的设计与运行,与硬件系统及其所处环境的数学模型和物理模型密不可分,不可避免地会涉及大量数值运算。许多可信性质或缺陷均与程序的数值性质密切相关,比如除零错、算术溢出、数组越界等常见的运行时错误。因此,对程序中数值相关性质进行分析,自动获取程序中变量之间的数值约束关系,对于整个安全攸关软件系统的可信性保证至关重要。抽象解释作为一种在程序分析和验证领域广泛使用的有效的静态分析方法,为程序数值性质的自动分析提供了一个通用框架。基于抽象解释的程序分析通过轻量级的抽象域表示和抽象域操作来刻画程序的状态和行为,具有较小的分析代价和较好的可扩展性。但基于抽象解释的轻量级分析常常会造成精度损失,甚至导致误报。另一方面,可满足性模理论（Satisfiability Modulo Theories,SMT）基于析取、量词等连接子和丰富的理论域可描述较强的约束表示,并可对基本程序块的迁移语义进行精确刻画。但基于SMT的方法计算复杂度较高,且难以有效处理循环。因此,本文将两者进行优势互补,研究结合SMT与抽象解释的程序分析技术,在分析精度和效率之间进行有效权衡。本文的主要贡献包括:1)提出了结合SMT的块级抽象解释框架。该框架针对语句级抽象解释存在的精度受限问题,将SMT与抽象域在框架内进行有效结合。块级抽象解释框架首先将程序划分成块,在程序块内使用表达能力更强的SMT刻画程序语义,在程序块间使用计算效率更高的抽象域传递程序语义,并在程序块的入口和出口处进行相互转换。该框架在整体上仍基于“迭代+加宽”的框架求解程序的不动点,即在加宽点处使用抽象域的加宽操作加速迭代收敛。此外,本文从精度和效率两个方面对块级抽象解释框架进行提升:在精度提升方面,设计了基于谓词划分的抽象域提升算子,向后续分析传递必要且更丰富的信息;在效率改进方面,提出了基于块级稀疏性的大块切割方法,有效地缓解复杂SMT公式的求解开销。对SV-COMP中程序进行分析的实验结果表明,基于结合SMT的块级抽象解释方法能够验证的性质大约是基于经典语句级抽象解释方法的两倍。2)提出了基于后向策略迭代的不动点求解算法。该算法针对策略迭代过程效率较低的问题,在“猜测+验证”的框架下对循环不动点进行求解。后向策略迭代算法首先基于SMT规划快速求得模版下的一个最小不动点候选;再基于SMT和线性规划技术验证其可行性;若该候选可行,则算法求得模版下的最小不动点;若该候选不可行,则算法重新求解一个新的最小不动点候选。然后本文对算法的正确性进行证明并对算法的复杂度进行分析。本文将此算法应用于面向性质验证的程序分析中,并提出了性质制导的后向策略迭代算法。性质制导的后向策略迭代算法在分析过程中优先选取与性质相关的模版和策略,在求解不动点的过程中可尽早发现性质是否为可验证的,并提前终止迭代过程,因而具有更好的分析效率。在验证SV-COMP的程序性质的实验中,性质制导的后向策略迭代算法可以更快地完成分析过程。3)设计和实现了区间线性模版约束抽象域。该抽象域针对凸抽象域表达能力不足的问题,对经典的模版抽象域进行了区间拓展,可推导变量间的区间线性关系。区间线性模版约束抽象域基于区间线性约束的“弱解”解语义刻画抽象域域元素,并基于区间线性规划技术设计其域操作。几何上域元素与每个象限的交均是一个凸的模版多面体（可以为空）,因此域元素可以看作是一系列模版多面体的析取,从而可以表达非凸（甚至非联通）性质。此外,本文还研究了区间线性模版抽象域中区间模版的生成策略。实验结果表明,区间线性模版约束抽象域可以较好地刻画程序的非凸性质。