当今软件规模和复杂程度日趋增加,提高软件的可信性已成为软件工程领域研究的焦点,尤其是在国防、金融、医疗等安全攸关领域。许多安全攸关软件,一般与数学和物理模型紧密关联,从而不可避免地会涉及大量数值计算。因此,对程序的数值缺陷和性质进行分析和验证,对于提高安全攸关软件的可信性尤为重要。抽象解释是一种通用的抽象近似理论,它为程序语义的抽象和推理提供了一个统一的理论框架,并在程序分析与验证领域得到了广泛应用。基于单遍抽象解释的程序分析和验证技术具有分析结果可靠、可扩展性好等优点。但其不足在于抽象语义下的程序推导可能存在巨大精度损失,从而导致在程序缺陷分析时产生大量的误报或在性质验证时不完备。因此,本文基于输入域划分、语义函数松弛等技术提出了一个基于迭代抽象解释的分析和验证框架,并结合动态测试技术,以实现更高精度的程序分析和更加完备的性质验证。本文的主要贡献涵盖以下三个方面:1.提出了一个性质制导的基于迭代抽象测试和有界枚举测试的通用验证框架,以提升抽象解释的数值程序验证能力。抽象测试本质上是利用前向抽象解释分析结果判断性质是否成立,若性质无法判断再利用后向抽象解释分析对输入进行精化。当单遍抽象测试无法判断性质是否成立时,本文利用了程序结构和验证性质制导的动态划分技术,将抽象输入划分成若干个子抽象输入。一方面由于每个子抽象输入对应的程序涉及较少、较简单的具体行为,故较易于被抽象测试验证;另一方面当子抽象输入域足够小时,本文利用有界枚举测试来实现完备的验证。抽象测试和具体测试是两项互补的验证技术,二者在本文的验证框架中实现了有效的结合。基于本文提出的验证框架实现了工具VATer,与单遍抽象解释分析工具相比,在测试集上VATer的验证成功率最高提升了3倍;而与当前最出色的三个基于模型检验的验证工具相比,VATer平均获得了数十倍的验证加速比。实验结果展示了VATer的验证有效性和高效性。2.提出了基于语义迁移函数松弛技术的层次化迭代抽象解释分析方法,以提高给定程序的不变式生成精度。循环是程序分析中最具挑战的结构之一,它也是抽象解释分析过程中精度损失的主要来源之一。本文的方法首先基于变量依赖关系的变量层次图,构建程序的逐层分析序列,再迭代利用低层程序中已计算出来的部分不变式（只涉及部分程序变量的不变式）对高层程序的迁移函数进行语义松弛,再对松弛之后的程序进行分析,最终提高对整个带循环程序的分析精度。迁移函数的松弛操作是本文方法的核心操作,本文提出并结合了多种松弛策略,以提升方法的整体精度提升效果。基于上述方法,本文实现了一个工具原型Relax AIer。相比单遍抽象解释分析工具Interproc,在测试集上Relax AIer所产生的循环不变式中包含的有界变量数是Interproc的4.78倍。实验结果表明Relax AIer显著提升了抽象解释分析的精度。3.提出了一种基于迭代抽象分析的神经网络验证框架,实现了既可靠又完备的神经网络验证。神经网络也可以看作是一类特殊的程序,本文将程序分析与验证的技术应用到神经网络的安全性和鲁棒性验证中,利用输入划分技术设计了基于迭代抽象验证的通用框架。考虑神经网络自身的特征,本文方法的核心思想是基于非确定首层（FUL）神经元产生输入域划分谓词使隐含层神经元中非确定状态的激活函数变为确定化状态,并将划分谓词进一步用于输入精化,全面提高基于松弛迁移语义的神经网络抽象分析的精度,实现高效验证的目标。验证过程中也结合了动态测试技术来快速寻找性质不成立的反例。本文实现了一个既可靠又完备的并行化的神经网络验证工具INDICATOR,并开展了充分实验对其进行评估。实验结果表明,与三个当前验证效果最好的既可靠又完备的验证工具Relu Val,Planet和Marabou相比,INDICATOR以更少的时间开销完备地验证了更多的性质。且在验证ACAS Xu神经网络中的性质时,INDICATOR较这三个工具分别获得了至少43倍,324倍和317倍的验证加速比。