一句话：提出基于量词的状态合并方法，通过动态分组和专用求解过程减少约束编码爆炸。
符号执行中的状态合并会因路径约束编码膨胀而难以应用，尤其是合并时引入大量析取与 if-then-else 表达式。本文提出一种带量词的状态合并方法：先动态检测符号状态路径约束中相似的统一结构，将状态划分到合并组，再用量词高效编码合并后的路径约束与内存。为应对量词约束求解的额外复杂度，作者设计专用求解过程以减少求解时间。实验评估表明，该方法在许多情况下带来显著性能提升。
We address the problem of constraint encoding explosion which hinders the applicability of state merging in symbolic execution. Specifically, our goal is to reduce the number of disjunctions and if-then-else expressions introduced during state merging. The main idea is to dynamically partition the symbolic states into merging groups according to a similar uniform structure detected in their path constraints, which allows to efficiently encode the merged path constraint and memory using quantifiers. To address the added complexity of solving quantified constraints, we propose a specialized solving procedure that reduces the solving time in many cases. Our evaluation shows that our approach can lead to significant performance gains.