对大规模软件时序性质进行自动验证是一项十分有意义的研究工作。本课题以抽象解释理论中的抽象逼近方法作为基本理论工具，利用有效的数学计算工具软件，基于抽象-精化的迭代验证框架，以验证软件时序性质的高效抽象验证方法作为主要研究内容，需要解决的理论问题有：大规模软件面向验证性质的抽象迁移模型自动构造，不同抽象层次程序不变式的自动构造，包括安全性、活性性质在内的时序性质面向性质的一体化自动验证方法，基于虚假反例的抽象精化方法。在此基础上，基于函数式程序设计语言Objective-Caml,设计并实现支持大规模软件时序性质自动验证的工具原型系统。