--- res: bibo_abstract: - 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, bisimulation minimization, circular assume-guarantee reasoning, and parametric reasoning about an unbounded number of threads. 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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Thomas A foaf_name: Thomas Henzinger foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Ranjit foaf_name: Jhala, Ranjit foaf_surname: Jhala - foaf_Person: foaf_givenName: Ritankar foaf_name: Majumdar, Ritankar S foaf_surname: Majumdar bibo_doi: 10.1145/996841.996844 dct_date: 2004^xs_gYear dct_publisher: ACM@ dct_title: Race checking by context inference@ ...