  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.
