Program Slicing

Program slicing is a technique for identifying portions of a program that can influence the way in which a collection of designated statements execute. For the purpose of model construction, we can use slicing to automate the process of eliminating portions of a program from a model without affecting the precision of the model. The idea is to extract a safe slicing criterion from the specification to be checked, e.g., temporal logic formulae. For example, this process may identify the set of statements that can directly influence the truth or falsity of the propositions in the formula. Slicing on such a criteria leaves a resulting program that preserves all of the relevant information for the behaviors of interest as defined by the specification. This sliced program is used as a starting point for the abstraction and specialization process.

Since we are interested in slicing concurrent Java programs we have found it necessary to extend the notions of of dependency found in the literature to properly account for intra-thread synchronization and data access.

As with most static analyses, slicing is a syntactic analysis that incorporates small bits of semantic information. For this reason, the precision of slicing, i.e., its ability to produce the smallest suitable program, can in some cases be less than is desired for model construction. We have defined some simple static analyses that can be run as a pre-phase to slicing that improve its precision by refining the dependence relations on which it is based.