Reference:

Dejvuth Suwimonteerabuth, Javier Esparza, and Stefan Schwoon. Symbolic context-bounded analysis of multithreaded java programs. In Klaus Havelund and Rupak Majumdar, editors, Proceedings of SPIN 2008, volume 5156 of Lecture Notes in Computer Science, pages 270–287, Los Angeles, USA, 2008. Springer.

Abstract:

The reachability problem is undecidable for programs with both recursive procedures and multiple threads with shared memory. Approaches to this problem have been the 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 not 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.

Suggested BibTeX entry:

@inproceedings{SES08,
    address = {Los Angeles, USA},
    author = {Dejvuth Suwimonteerabuth and Javier Esparza and Stefan Schwoon},
    booktitle = {Proceedings of SPIN 2008},
    editor = {Klaus Havelund and Rupak Majumdar},
    pages = {270-287},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Symbolic Context-Bounded Analysis of Multithreaded Java Programs},
    volume = {5156},
    year = {2008}
}