Exploring Loose Coupling of Slicing with Dynamic Symbolic Execution on the JVM

Dynamic symbolic execution is an effective technique for fuzzing programs with application to software verification as well if the search terminates during symbolic execution. However, the state space explosion problem often prevents the symbolic search from exploring the entire state space. As static analysis operates on the whole program rather than single execution paths, it can cut out parts of the program that are irrelevant for verifying a property. In this paper, we explore how slicing can be used before dynamic symbolic execution for analyzing assertion reachability in Java programs. We report on our first experience using state-of-the-art open-source Java slicers on the SV-COMP Java benchmark before applying GDart, a dynamic symbolic execution engine for Java. Currently, this experiment has not been successful, as the slicers are not mature enough to reliably produce correct slices of a task in the SV-COMP benchmark. However, in a few examples, the approach delivered promising results that motivate the future development of slicers for Java.