Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar
Software model checking has been successful for sequential programs, where predicate abstraction offers suitable models, and counterexample-guided abstraction refinement permits the automatic inference of models. When checking concurrent programs, we need to abstract threads as well as the contexts in which they execute. Stateless context models, such as predicates on global variables, prove insufficient for showing the absence of race conditions in many examples. We therefore use richer context models, which combine (1) predicates for abstracting data state, (2) control flow quotients for abstracting control state, and (3) counters for abstracting an unbounded number of threads. We infer suitable context models automatically by a combination of counterexample-guided abstraction refinement, minimization, circular assume-guarantee reasoning, and parametric reasoning. This algorithm, called CIRC, has been implemented in Blast and succeeds in checking many examples of NESC code for data races. In particular, Blast proves the absence of races in several cases where previous race checkers give false positives.
Proceedings of the International Conference on Programming Language Design and Implementation (PLDI), ACM Press, 2004, pp. 1-13.