论文下载：https://www.comp.nus.edu.sg/~joxan/papers/testing.pdf
ABSTRACT && INTRODUCTION
- 优化concolic execution的工作
- 当前的优化方法：启发式搜索策略、简易功能缓存、动静结合
- 作者提出搜索剪枝的方法：如果一个test遍历了一条路径，当下次另一test遇到相同情况的时候就可实现剪枝
- concolic execution(我是传送门)
RUNNING EXAMPLE
- 假设两个read()都非0，程序执行到l_8，路径可达，没有bug
- 反转l_6的条件，发现不可达，所以l_6这个subtree搜索完成，条件是s <=3（这个例子有点违和，在符号执行里面放bug不可达）
- 回溯，到l_4，发现分支l’_6，但条件是s < = 1，满足刚才l_6的条件，所以不用再搜索
- l_4搜索完全，条件是s < = 1
- …
ALGORITHM
- 每当产生一条新的路径，就检查是否被搜索过
- 如果没有被搜索过，就执行concolic execution，但会记录每个分支的搜索条件和情况，即SymExec这个过程
- SymExec包括回溯的过程，对于回溯的搜索作了限定：每个program point只被搜索至多一次，当再次经过的时候，检查是否可以被剪枝，如果不行，放弃回溯
- 保证回溯是O(n)
Evaluation
- 4 programs from the ntdrivers-simplified category of SV-COMP’12
- 1000 – 2000 LOC
- 控制流复杂，有大量路径
Performance
- b明显说明回溯的作用
Subsumption
- 剪掉的路径数量百分比
Extra path-coverage
- 隐含福利，回溯的时候存在额外搜索，作为主搜索的补充
- （作者没有说明数据获取细节，但这个福利未免太大了）
