




Publications  Symbolic ContextBounded Analysis of Multithreaded Java Programs





Reference:
Dejvuth Suwimonteerabuth, Javier Esparza, and Stefan Schwoon. Symbolic contextbounded 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, August 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 contextbounded 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, contextbounded reachability has not been implemented in any tool so far, primarily because its worstcase runtime is prohibitively high, i.e. O(n^k), where n is the size of the shared memory. Moreover, existing algorithms for contextbounded reachability do not admit a meaningful symbolic implementation (e.g., using BDDs) to reduce the runtime 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},
month = {August},
pages = {270287},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Symbolic ContextBounded Analysis of Multithreaded Java Programs},
volume = {5156},
year = {2008}
}




