Program slicing [1] is a technique for extracting those sentences of a program that affect or are affected by a given slicing criterion. Since this technique was introduced in 1984, many other approaches (such as constraint slicing and hybrid slicing) have appeared in order to solve different problems that possible applications of it present.

This paper identifies two questions that remain unsolved by previous techniques: “For every program point, under which variable values does the program point affect the slicing criterion?” “For every program point, does the program point affect the slicing criterion if we are only interested in certain executions of the program rather than all possible ones?”

The authors address both problems by proposing a new data structure to represent data and control flow relations of a program called an abstract state graph. This data structure is obtained by applying predicate abstraction to a program with predicates and constraints. While program dependence graphs—the usual data structure used in program slicing—could also be used for abstract slicing, in practice, it would not be suitable because of the state explosion problem. In order to overcome this, the authors reduce abstract slicing to a least fixpoint computation over computational tree logic (CTL) formulas so that symbolic model checkers for CTL can be used.

The technique, which is a generalization of static slicing, accepts forward slicing, backward slicing, and chopping slicing criteria. It presents an algorithm (without a soundness or completeness proof) to perform abstract slicing. The paper includes a description of the implementation and a summary of some experiments carried out with a number of benchmarks that clearly show the exponential growth in the number of states.

The paper is well written, easy to follow, and presents a good motivating example that shows the advantage of abstract slicing over traditional static slicing.