在模型检测的逻辑基础、算法设计、工具实现与实例应用三个层面上进行了深入研究，取得了多项成果，包括CTL的限界语义和基于该限界语义和QBF公式的正确性判定的模型检测方法、基于形式语言理论和反例制导的抽象求精方法的并发递归程序安全性质的自动验证、Applied Pi-演算的符号互模拟理论、带参系统的模型检测的状态聚类和数组截断方法、以及模型检测技术在DSP系统和CPU设计功能验证的实例研究。.基于所取得的理论成果，实现了包括集限界模型检测和符号模型检测方法于一体的模型检测工具VERDS、存储一致性验证工具MOTEC、带参模型检测工具PaMC。这些原型工具为今后的研究工作提供了平台和基础。.项目执行期间开展了高层次的学术交流。组织了2次国际学术讲习班，有240多人次参加，推动了国内在模型检测领域的研究。发表学术论文50篇；培养博士16名、硕士4名、出站博士后1名。全面实现了项目的预定研究目标。