基于符号执行的复杂软件系统测试与验证研究

近年来符号执行技术成为大力推动软件测试与验证领域研究工作的热点之一。面对复杂软件系统的测试与验证需求，当前符号执行技术受困于两大主要障碍：一是大规模程序状态空间的制导遍历，二是包含复杂程序特征（浮点计算、非线性约束、第三方库函数调用等）的约束问题求解。..本项目以突破符号执行技术面临的这两大障碍为主线，基于符号执行技术解决测试用例生成、程序行为自动分析、代码有界模型检验中的关键问题，进一步提升相关测试和验证技术与工具的有效性和可扩展性。具体研究内容包括面向深度覆盖的符号执行制导、面向复杂程序特征的测试用例生成、面向复杂性质的程序行为自动检测、基于程序路径编码和遍历的有界模型检验。

Symbolic Execution is one of the most important topics which promote the research of software testing and verification. There are two main obstacles which restrict the analysis of complex software systems by symbolic execution. First, guided traversing of large scale state space of software code. Second, the constraint solving of code with complex characteristics, e.g. floating point computations, nonlinear constraints, third party function calls. ..The main research threads of this project is organized to break through the above two obstacles. This project attacks the key problems behind symbolic execution based test generation, automatic analysis of program behavior and bounded model checking of software code, and will increase the efficiency and scalability of software testing and verification techniques and tools. In detail, the research problems of this project include: deep behavior coverage guided symbolic execution, test case generation with complex program characteristics, complex property guided code behavior detection, and path encoding and traversing based code bounded verification.