Program slicing is a technique to extract relevant parts of a program, and it is widely used in program debugging, parallelization, testing, reverse engineering, etc. This paper concerns \emph{static slicing\/} and it follows the Weiser's definition of slicing that consists of computing what statements of the program might affect the value of some particular variable at a specified program point. We argue that although there is a broad variety of static slicing methods, it is commonly assumed that all paths are executable. However, this limitation may be completely unacceptable in, for instance, debugging and program understanding tasks since the slice is often quite big.
In this paper, we present a fully \emph{path-sensitive\/} slicing that identifies infeasible paths in order to obtain accurate slices. Infeasible paths are detected by performing symbolic execution of the program. The major challenge is that in general there are exponentially many paths. Our method traverses the symbolic execution tree, in a post-order manner, and discovers an \emph{interpolant\/} which generalizes the execution context of the tree. This enhances the likelihood that the \emph{dependencies} computed for that tree can be \emph{reused\/} in multiple contexts.
Another key feature is that our algorithm stores, for each dependency, the executable path that defines it, that is, the \emph{representative path formula\/} that gives rise to it. By doing so, the dependency information is accurate since it is only used if the new context demonstrates that the representative is executable. In fact, for loop-free programs, our algorithm computes \emph{exactly} the statements relevant to the slicing criterion.