一句话：提出对循环内状态进行剪枝的符号执行技术，在保持代码覆盖率的同时缓解路径爆炸。
符号执行长期受路径爆炸困扰：循环内的分支在每次迭代都可能产生新状态，大量路径对代码覆盖率并无贡献，却使执行难以到达程序更深的部分。本文提出以状态剪枝来削减循环内路径的思路，核心是在循环中限制所生成路径的数量，而非为每条可行执行路径都建立符号路径。通过识别并剪除对覆盖率无贡献的循环内状态，该方法试图在维持高代码覆盖率的前提下抑制路径数量增长，从而让符号执行能够继续深入程序内部。摘要给出了问题动机与方法思路，但未报告具体的实现细节与实验数据。
Path explosion has been a problem for symbolic execution for a long time. The key to avoid path explosion is to limit the number of paths generated within loops while maintaining high code coverage. Full symbolic execution creates paths for every possible execution path. Frequently, paths within loops do not contribute to code coverage. Branches within loops may generate new states at every iteration. The path explosion problem created by loops often stops symbolic execution to reach deeper parts of the code.
DOI 原文 ·
@inproceedings{paperbot4797,
title = {Loop path reduction by state pruning},
author = {Jianxiong Gao and Steven S. Lumetta},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3240731}
}