一句话：将符号执行划分为两阶段，用第一阶段公式在线合成SMT求解策略以提升后续约束求解效率。
符号执行由约束求解驱动，而现代SMT求解器提供的求解策略机制允许用户控制求解过程，显著提升求解器的泛化能力。论文观察到不同程序的符号执行实际上对应不同的约束求解问题，因此提出为每个程序合成一个最契合其符号执行的求解策略。作者将符号执行分为两个阶段：第一阶段求解得到的SMT公式用于在线合成求解策略，该策略随后在第二阶段的约束求解中使用。论文提出新的合成算法，将离线训练的深度学习模型与在线调优相结合来生成求解策略，并在合成开销与所合成策略带来的求解改进之间取得平衡。
Symbolic execution is powered by constraint solving. The advancement of constraint solving boosts the development and the applications of symbolic execution. Modern SMT solvers provide the mechanism of solving strategy that allows the users to control the solving procedure, which significantly improves the solver's generalization ability. We observe that the symbolic executions of different programs are actually different constraint solving problems. Therefore, we propose synthesizing a solving strategy for a program to fit the program's symbolic execution best. To achieve this, we divide symbolic execution into two stages. The SMT formulas solved in the first stage are used to online synthesize a solving strategy, which is then employed during the constraint solving in the second stage. We propose novel synthesis algorithms that combine offline trained deep learning models and online tuning to synthesize the solving strategy. The algorithms balance the synthesis overhead and the improvement achieved by the synthesized solving strategy.
DOI 原文 ·
@inproceedings{paperbot6683,
title = {Synthesize solving strategy for symbolic execution},
author = {Zhenbang Chen and Zehua Chen and Ziqi Shuai and Guofeng Zhang and Weiyu Pan and Yufeng Zhang and Ji Wang},
booktitle = {ISSTA},
year = {2021},
doi = {10.1145/3460319.3464815}
}