---
_id: '4459'
abstract:
- lang: eng
  text: 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.
author:
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
citation:
  ama: 'Henzinger TA, Jhala R, Majumdar R. Race checking by context inference. In:
    ACM; 2004:1-13. doi:<a href="https://doi.org/10.1145/996841.996844">10.1145/996841.996844</a>'
  apa: 'Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). Race checking by context
    inference (pp. 1–13). Presented at the PLDI: Programming Languages Design and
    Implementation, ACM. <a href="https://doi.org/10.1145/996841.996844">https://doi.org/10.1145/996841.996844</a>'
  chicago: Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Race Checking
    by Context Inference,” 1–13. ACM, 2004. <a href="https://doi.org/10.1145/996841.996844">https://doi.org/10.1145/996841.996844</a>.
  ieee: 'T. A. Henzinger, R. Jhala, and R. Majumdar, “Race checking by context inference,”
    presented at the PLDI: Programming Languages Design and Implementation, 2004,
    pp. 1–13.'
  ista: 'Henzinger TA, Jhala R, Majumdar R. 2004. Race checking by context inference.
    PLDI: Programming Languages Design and Implementation, 1–13.'
  mla: Henzinger, Thomas A., et al. <i>Race Checking by Context Inference</i>. ACM,
    2004, pp. 1–13, doi:<a href="https://doi.org/10.1145/996841.996844">10.1145/996841.996844</a>.
  short: T.A. Henzinger, R. Jhala, R. Majumdar, in:, ACM, 2004, pp. 1–13.
conference:
  name: 'PLDI: Programming Languages Design and Implementation'
date_created: 2018-12-11T12:08:57Z
date_published: 2004-06-01T00:00:00Z
date_updated: 2021-01-12T07:57:07Z
day: '01'
doi: 10.1145/996841.996844
extern: 1
month: '06'
page: 1 - 13
publication_status: published
publisher: ACM
publist_id: '271'
quality_controlled: 0
status: public
title: Race checking by context inference
type: conference
year: '2004'
...