Previous work has shown that program slicing can be a useful step in model-checking software systems. We are interested in
applying these techniques to construct models of multi-threaded Java programs. Past work does not address the concurrency
primitives found in Java, nor does it provide the rigorous notions of slice correctness that are necessary for reasoning about
programs with non-deterministic behaviour and potentially infinite computation traces.
In this paper, we define the semantics of a simple multi-threaded language with concurrency primitives matching those found
in the Java Virtual Machine, we propose a bisimulation-based notion of correctness for slicing in this setting, we identify
notions of dependency that are relevant for slicing multi-threaded Java programs, and we use these dependencies to specify
a program slicer for the language presented in the paper. Finally, we discuss how these dependencies can be refined to take
into account common programming idioms of concurrent Java software.
This work supported in part by NSF under grants CCR-9633388, CCR-9703094, CCR-9708184, and CCR-9701418 and DARPA/NASA under
grant NAG 21209.