Selected publications by Stefan Schwoon

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(nk), 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.

@inproceedings{SES-spin08,
   address = {Los Angeles, California, USA},
   author = {Suwimonteerabuth, Dejvuth and Esparza, Javier and Schwoon, Stefan},
   booktitle = {{P}roceedings of the 15th {I}nternational {SPIN} {W}orkshop on {M}odel {C}hecking {S}oftware ({SPIN}'08)},
   DOI = {10.1007/978-3-540-85114-1_19},
   editor = {Havelund, Klaus and Majumdar, Rupak and Palsberg, Jens},
   month = aug,
   pages = {270-287},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Symbolic Context-Bounded Analysis of Multithreaded {J}ava Programs},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SES-spin08.pdf},
   volume = {5156},
   year = {2008},
}

About LSV