To make the developer’s life easier, many tools have been created for analyzing source code. Such analysis can be used, for example, to detect bugs, to check the coverage of a set of tests, or even to generalize testing by using symbolic variables in execution. This latter point, symbolic execution, explores all the paths of a given code snippet and generates the test inputs. Symbolic execution is a technique that helps evaluate whether certain formulas and properties defined in the code are satisfiable; for example, is this code reachable? Such properties are usually given using logics.

However, programs are complex. The practical usage of symbolic execution is jeopardized by the problem of path explosion, that is, “the number of explored paths usually grows exponentially with the increase of program size.” Even a program of medium size (around 4,000 lines of code) becomes very hard to handle.

The authors’ intuition is that some paths are not necessarily useful to be explored, since their behavior can be assimilated by other paths, effectively creating a path dependency. Their approach is to exploit such dependencies to “guide path exploration so that the redundant paths can be predicted and eliminated.” The authors also prove that their approach has the same fault detection capabilities as traditional symbolic execution techniques, assuming a code style is defined.

The paper contains a very useful part on related works, which readers who are less familiar with the technique may use to get further links to research papers and tools. The authors provide the source code of the experiments and their implementation has been executed with a suite, widely used as input for software testing and fault localization tasks.