程序验证是保证程序正确性的关键技术。停机性和安全性验证是程序验证中的两个重要研究内容,受到了大量关注和广泛研究。本文针对程序的停机性和安全性验证进行了系统、深入的研究,主要工作包括以下几个方面:1.基于最优化问题提出了一种线性秩函数构造技术。首先设置线性秩函数模板和模板中参数的取值区间,并在取值区间内对线性秩函数模板中的参数进行实例化,然后以循环不变式作为最优化问题的约束系统,以实例化的线性秩函数模板的差分作为最优化问题的目标,构造最优化问题并进行求解。最优化问题的最优解给出了线性秩函数递减的最小步长,因而可以进一步应用于计算循环精确的符号化复杂度上界。基于最优化问题的秩函数构造方法不但能够验证线性程序和多项式程序的停机性,而且可以验证某些含有指数或对数函数的非多项式程序的停机性。2.基于不变式生成技术提出了验证程序停机性和安全性的框架。将程序不变式视为程序变量的约束系统。通过引入不变式集,给出了验证程序停机性和安全性的新方法。通过插桩循环计数器将循环停机性的验证转化为求解一个最优化问题,其中最优化问题的约束系统为循环出口的所有程序不变式集合,最优化问题的目标函数是计算循环计数器的最小值。使用这种方法,将不再需要求解秩函数,并且对某些不存在秩函数的循环也可以验证其停机性。本文还提出了基于定理证明器验证逻辑蕴涵关系的安全性验证方法,将安全性的验证转化为验证不变式集合是否蕴含由描述安全性的逻辑公式。由于在每个程序点都可以生成不变式集合,不需要采用计算最弱前置条件,降低了自动验证的难度。3.基于差分方程和最优化问题,提出了一种循环符号化复杂度上界的计算方法。循环符号化复杂度上界是循环执行次数的一个符号化上界,它可以衡量程序的时间复杂度,也可以用于验证程序的停机性。首先用差分方程刻画循环中变量取值的变化,并求解出差分方程的闭合形式解。然后以差分方程的闭合形式解和循环条件取反作为最优化问题的约束系统,以表示循环执行次数的变量作为最优化问题的目标,构造最优化问题并进行求解。最优化问题的解就是循环符号化复杂度上界。这种方法可以验证不存在秩函数并且不存在多项式等式循环不变式的程序的停机性,与其他工作比较,基于差分方程和最优化问题能够给出更精确的符号化复杂度上界。4.条件停机验证的目的是构造程序停机的前置条件。基于polyranking方法和约束求解,提出了一种条件停机验证方法,对于具有阶段变化(phase-change)的程序,能够直接计算出所期望的停机前置条件,与其他方法相比,具有更好的计算效率。