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 the context of a thread. Stateless context models, such as predicates on global variables, prove insufficient for showing the absence of race conditions in many examples we looked at. 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 umbounded 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 26th Annual Conference on Programming Language Design and Implementation (PLDI), ACM Press, 2004.