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.
- Honing the Detection of Interference and Ready Dependence for Slicing Concurrent Java Programs.
Venkatesh Prasad Ranganath, John Hatcliff. July 2003, Technical Report, SAnToS
-TR2003-6. Last updated: July 14, 2003.
- Slicing Software for Model Construction (June 1999), Matthew B. Dwyer, John Hatcliff, Hongjun Zheng, To appear in a special issue of the Journal of Higher-order and Symbolic Computation dedicated to selected papers from the 1999 ACM SIGPLAN Partial Evaluation and Program Manipulation, January, 1999.
- A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives, John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, and Hognjun Zheng, in Proceedings on the 1999 International Symposium on Static Analysis, Lecture Notes in Computer Science 1694, Sept, 1999.
- Slicing Multi-threaded Java Programs : A Case Study, Matthew B. Dwyer, James C. Corbett, John Hatcliff, Stefan Sokolowski, and Hognjun Zheng, This paper is published as KSU CIS TR 99-7.