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.