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求解的计算复杂度造成的。本文提出一种面向符号执行的分治方法，通过分别执行切片并随后合并副作用。通过这种方式，整体问题规模得以保持较小状态，从而降低了计算复杂度对大型问题的影响。