中文摘要：

对大规模软件时序性质进行自动验证是一项十分有意义的研究工作。本课题以抽象解释理论中的抽象逼近方法作为基本理论工具，利用有效的数学计算工具软件，以验证软件时序性质的高效抽象验证方法作为主要研究内容，重点研究了不变式构造技术、基于不变式构造和定理证明器的安全性验证方法、秩函数构造方法、综合多种方法的软件停机性验证方法。在此基础上,基于数学符号计算工具Mathematica6.0和定理证明系统Theorema以及函数式程序设计语言Objective Caml，设计并实现了一个软件验证支持环境，能够对一些数值计算程序的不变式断言、停机性和部分正确性进行自动验证。