Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities. Compared to other testing methods such as fuzzing, Symbolic Execution has the advantage of providing formal guarantees about the program. However, despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software. This is primarily caused by the \emph{path explosion problem} as well as by the computational complexity of SMT solving. In this paper, we present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects. This way, the overall problem size is kept small, reducing the impact of computational complexity on large problems.

翻译：符号执行是一种可用于验证计算机程序行为并检测软件漏洞的形式化方法。与模糊测试等其他测试方法相比，符号执行具有提供程序形式化保证的优势。然而，尽管近年来性能有所提升，符号执行仍因速度过慢而难以应用于实际软件。这主要是由路径爆炸问题以及SMT求解的计算复杂性导致。本文提出了一种分治方法的符号执行方案：通过执行独立切片并随后合并副作用来达成目标。这种方式使得整体问题规模保持较小，从而降低了计算复杂性对大问题的影响。