基于程序综合的符号执行环境建模方法研究

项目名称： 基于程序综合的符号执行环境建模方法研究

项目编号： No.61402454

项目类型： 青年科学基金项目

立项/批准年度： 2014

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

项目作者： 王立泽

作者单位： 中国科学院软件研究所

项目金额： 25万元

中文摘要： 环境建模已成为阻碍符号执行发展的瓶颈之一。在航天、航空等对软件质量提出迫切要求的领域，环境模型的有效搭建将更有利于发现软件缺陷，提升可靠性和安全性。本课题主要利用程序综合技术解决符号执行环境模型的代码自动生成问题。具体步骤如下：1）对环境程序进行领域分析，识别并抽象其高层行为，转化为对抽象数据结构的操作，结合组件技术，建立满足符号执行要求的环境模型组件库；2）利用机器学习、组件检索技术，对组件库求精以缩小搜索空间；3）通过程序综合技术，给定环境程序二进制代码，应用采样机制建立规格描述，结合组件库以限定搜索空间，设计优化的搜索技术，利用约束求解器进行求解，并迭代执行，最终获取环境模型的完整代码；4）分析、验证建模方法的副作用。课题从模型的通用性入手，从行为抽象角度阐明精简模型实现技术，从程序综合角度提出一种新的符号执行环境模型建模方法，为环境建模问题的进一步研究与应用提供新思路和理论依据。

中文关键词： 符号执行；环境建模；程序综合；；

英文摘要： Environmental modeling has become one of the bottlenecks of symbolic execution. The effective solution of this problem is beneficial to find software defect and improve the reliability and safety in areas of aerospace, aviation, etc., which have an urgent

英文关键词： Symbolic Execution；Environment Modeling；Program Synthesis；；