一句话：将 veritesting 的路径合并思想扩展到 Java 符号执行，通过静态摘要控制流区域缓解路径爆炸。
符号执行面临路径爆炸问题，合并执行路径是一种有效的缓解手段。Avgerinos 等人提出的 veritesting 将有界控制流区域转换为单一约束，从而在既有的单路径符号执行引擎上实现路径合并；但此前工作主要面向二进制代码，Java 语言需要不同的设计考量。本文把这一思路扩展到 Java 符号执行，提出 Java Ranger，通过静态摘要区域来合并路径并提升效率。摘要未报告具体实验数据，核心贡献是面向 Java 的机制设计、实现与扩展。
Merging execution paths is a powerful technique for reducing path explosion in symbolic execution. One approach, introduced and dubbed “veritesting” by Avgerinos et al., works by translating abounded control flow region into a single constraint. This approach is a convenient way to achieve path merging as a modification to a pre-existing single-path symbolic execution engine. Previous work evaluated this approach for symbolic execution of binary code, but different design considerations apply when building tools for other languages. In this paper, we extend the previous approach for symbolic execution of Java.
DOI 原文 ·
@inproceedings{paperbot5834,
title = {Java Ranger: statically summarizing regions for efficient symbolic execution of Java},
author = {Vaibhav Sharma and Soha Hussein and Michael W. Whalen and Stephen McCamant and Willem Visser},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3409734}
}