Title: 
  A Formal Study of Slicing for Multi-threaded Programs 
  with JVM Concurrency Primitives

Speaker:
  John Hatcliff
  Kansas State University

Abstract:

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.  The
slicing literature contains some work on slicing multi-threaded
programs, but this 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 talk, we define the semantics of a simple multi-threaded
language with concurrency primitives matching those found in the Java
Virtual Machine.  Using this semantics, we propose a
bisimulation-based notion of correctness for slicing in this setting.
Building on existing notions of dependency in the slicing literature,
we identify additional dependencies that are relevant for slicing
multi-threaded Java programs, and we use these dependencies to 
specify a program slicer for the language presented.
We discuss how these dependencies can be refined to 
take into account common programming idioms of concurrent Java software.

Finally, we discuss the mechanics of incorporating slicing techniques
into Bandera -- a tool set for model-checking software systems.