| 形状分析符号执行引擎中的状态合并 |
| |
| 引用本文： | 邓维,李兆鹏.形状分析符号执行引擎中的状态合并[J].计算机科学,2017,44(2):209-215. |
| |
| 作者姓名： | 邓维 李兆鹏 |
| |
| 作者单位： | 中国科学技术大学计算机科学技术学院 合肥230026 中国科学技术大学先进技术研究院中国科大-国创高可信软件工程中心 合肥230027,中国科学技术大学计算机科学技术学院 合肥230026 中国科学技术大学先进技术研究院中国科大-国创高可信软件工程中心 合肥230027 |
| |
| 基金项目： | 本文受国家自然科学基金项目(61229201,8,91318301)资助 |
| |
| 摘 要： | 符号执行技术以其良好的精确度控制和代码覆盖率被广泛应用于静态程序分析和高覆盖率测试用例自动生成。 符号执行 在分析程序时,以模拟真实的程序执行过程的方式分析程序的数据流和控制流信息,并检查程序可能出现的所有状态,得到程序的分析结果。高精确度和高覆盖率要求对程序状态描述具体而完备,这会导致符号执行过程中常见的状态爆炸问题。首先提出在不同的执行路径上对具体内存状态进行合并的算法,然后对内存模型进行适度的抽象,扩大状态合并算法的适用范围,最后讨论状态合并所带来的实际效果,并提出了状态合并的优化解决方案。所提出的算法在符号执行引擎ShapeChecker上实现,并取得了良好的实验结果。
|
| 关 键 词： | 符号执行 状态合并 求解代价 内存模型 状态抽象 |
| 收稿时间： | 2016/1/5 0:00:00 |
| 修稿时间： | 2016/4/10 0:00:00 |
State Merging for Symbolic Execution Engine with Shape Analysis |
| |
| DENG Wei and LI Zhao-peng.State Merging for Symbolic Execution Engine with Shape Analysis[J].Computer Science,2017,44(2):209-215. |
| |
| Authors: | DENG Wei and LI Zhao-peng |
| |
| Affiliation: | School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China USTC-Sinovate High Confidence Software Engineering Center,Institude of Advanced Technology, University of Science and Technology of China,Hefei 230027,China and School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China USTC-Sinovate High Confidence Software Engineering Center,Institude of Advanced Technology, University of Science and Technology of China,Hefei 230027,China |
| |
| Abstract: | |
| |
| Keywords: | Symbolic execution State merging Query cost Memory model State abstraction |
|
|
点击此处可从《计算机科学》下载全文 |
|
