Symbolic context-bounded analysis of multithreaded java']java programs

The reachability problem is undecidable for programs with both recursive procedures and multiple threads with shared memory. Approaches to this problem have been tire focus of much recent research. One of these is to use context-bounded reachability, i.e. to consider only those runs in which the active thread changes at most k times, where k is fixed. However, to the best of our knowledge, context-bounded reachability has riot been implemented in any tool so far,, primarily because its worst-case runtime is prohibitively high, i.e. O(n(k)), where n is the size of the shared memory. Moreover, existing algorithms for context-bounded reachability do not admit a meaningful symbolic implementation (e.g. using BDDs) to reduce the run-time in practice. In this paper, we propose an improvement that overcomes this problem. We have implemented our approach in the tool jMoped and report on experiments.