基于符号执行的并发程序分析与验证研究

项目名称： 基于符号执行的并发程序分析与验证研究

项目编号： No.61272140

项目类型： 面上项目

立项/批准年度： 2013

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

项目作者： 黄春

作者单位： 中国人民解放军国防科学技术大学

项目金额： 80万元

中文摘要： 随着并行计算和异构多核平台的应用越来越广泛，并发软件的质量引起了广泛关注。由于并发系统自身的非确定性，使得并发程序呈现出不可预测性、状态空间巨大、复杂性等特征,为并发系统的可信保障带来了巨大挑战。因此，研究并发程序的形式验证技术，对提高并发系统的可靠性与安全性具有重要意义。本项目将首先从并发程序的特点和可信需求出发，研究并发程序的错误特征和关键性质规约方法，得到能够支持并发程序交叠执行规约的多维形式规约方法；然后在规约方法的基础上，结合符号执行技术的最新进展，研究基于符号执行的分析验证技术及其优化，支持高效的并发程序验证；进一步研究符号执行的环境支持和数据结构抽象技术，提高验证方法可行性和完全性；最终建立自动化程度高、直接面向源代码的并发程序符号执行和验证工具。本项目的研究能显著提高并发程序的验证能力，能丰富和发展基于符号执行的程序分析与验证方法，为提高并发系统的可靠性提供有力支持。

中文关键词： 并发系统；并行程序；MPI；符号执行；分析验证

英文摘要： With the wide spread and application of parallel computing and heterogeneous multi-core platforms, the quality of concurrent software has been paid with more and more attention. Usually, a concurrent system is non-deterministic. In the result of the non-determinism, a concurrent program is unpredictable and complex, and has a huge state space, which makes it a great challenge to ensure the trustworthy of a concurrent system. Therefore, it is important to study the formal verification of a concurrent system for improving the reliability and security. This project will carry out the research as follows: first, with respect to the features and the trustworthy requirements of concurrent programs, we will investigate the bug features and the formal specification method of concurrent programs, which will result a multi-dimensional specification method that can support specifying the interleaving of a concurrent program; second, based on the specification method, we will research the analysis and verification techniques by leveraging symbolic execution, and the result is supposed to support the verification of concurrent programs with a high efficiency; third, we will study environment support and the abstraction of data structures for improving the feasibility and completeness of symbolic execution; last, we will impl

英文关键词： Concurrent systems；Concurrent programs；MPI；Symbolic execution；Analysis and Verification