Context-Bounded Model Checking of Concurrent Software

The interaction among concurrently executing threads of a concurrent program results in insidious programming errors that are difficult to reproduce and fix. Therefore, analysis techniques that can automatically detect errors in concurrent programs can be invaluable. This paper presents a new static analysis technique based on model checking for detecting safety errors in concurrent programs. The problem of checking safety properties on a single-threaded boolean program with an unbounded stack is decidable. However, the same verification problem for a multi-threaded boolean program is undecidable Ramalingam00. In this paper, we prove that the problem is decidable if the analysis is restricted to executions in which the number of context switches is bounded by an arbitrary constant. Restricting the analysis to executions with a bounded number of context switches is unsound. However, the analysis can still discover intricate bugs since within each context, a thread is fully explored for unbounded stack depth. Our algorithm works even in the presence of an unbounded number of dynamically allocated threads.