并发程序的精化验证技术及其关键应用

项目名称： 并发程序的精化验证技术及其关键应用

项目编号： No.61379039

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 冯新宇

作者单位： 中国科学技术大学苏州研究院

项目金额： 75万元

中文摘要： 精化验证是一种重要的程序验证技术，它在算法验证、编译器验证和操作系统验证等方向都有着重要的应用。然而，在并发环境下，现有的精化验证理论和技术尚有着很多缺陷，不能有效支持上述的应用需求，具体表现为活性验证需求和验证技术的可组合性无法兼顾、缺少对弱内存模型和带中断的并发等多种并发模型的支持、以及缺少公理化的证明理论和工具等。 针对上述不足，本课题研究并发程序的精化验证理论和技术，在坚持验证技术的模块化和可组合性的基础上，探讨在不同并发模型下的精化关系刻画和证明，加强对程序活性验证的支持，开发霍尔风格的公理化程序逻辑和证明系统，最终形成支持多种并发程序验证的统一的基础验证理论和框架。我们还将探讨该理论和框架在细粒度并发算法验证、软件事务型内存算法（一种并发编译技术）验证以及操作系统内核中的中断和调度机制验证方面的应用，以检验理论和框架的有效性和实用性。

中文关键词： 程序验证；并发；精化；程序逻辑；程序正确性

英文摘要： Program refinement has been used as a theoretical foundation for program verification, including algorithm verification, compiler verification and OS kernel verification. However, existing theories and verification techniques all have serious problems to

英文关键词： Program Verification；Concurrency；Refinement；Program Logic；Program Correctness