---
OA_type: closed access
_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.
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  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
  last_name: Majumdar
citation:
  ama: 'Henzinger TA, Jhala R, Majumdar R. Race checking by context inference. In:
    <i>Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design
    and Implementation</i>. Association for Computing Machinery; 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. In <i>Proceedings of the ACM SIGPLAN 2004 conference on Programming
    language design and implementation</i> (pp. 1–13). Washington, DC, United States:
    Association for Computing Machinery. <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.” In <i>Proceedings of the ACM SIGPLAN 2004 Conference on
    Programming Language Design and Implementation</i>, 1–13. Association for Computing
    Machinery, 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,”
    in <i>Proceedings of the ACM SIGPLAN 2004 conference on Programming language design
    and implementation</i>, Washington, DC, United States, 2004, pp. 1–13.
  ista: 'Henzinger TA, Jhala R, Majumdar R. 2004. Race checking by context inference.
    Proceedings of the ACM SIGPLAN 2004 conference on Programming language design
    and implementation. PLDI: Programming Languages Design and Implementation, 1–13.'
  mla: Henzinger, Thomas A., et al. “Race Checking by Context Inference.” <i>Proceedings
    of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation</i>,
    Association for Computing Machinery, 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:, Proceedings of the ACM SIGPLAN
    2004 Conference on Programming Language Design and Implementation, Association
    for Computing Machinery, 2004, pp. 1–13.
conference:
  end_date: 2004-06-11
  location: Washington, DC, United States
  name: 'PLDI: Programming Languages Design and Implementation'
  start_date: 2004-06-09
date_created: 2018-12-11T12:08:57Z
date_published: 2004-06-09T00:00:00Z
date_updated: 2026-05-29T09:37:45Z
day: '09'
doi: 10.1145/996841.996844
extern: '1'
fulldoi: https://doi.org/10.1145/996841.996844
language:
- iso: eng
month: '06'
oa_version: None
page: 1 - 13
publication: Proceedings of the ACM SIGPLAN 2004 conference on Programming language
  design and implementation
publication_identifier:
  isbn:
  - '1581138075'
publication_status: published
publisher: Association for Computing Machinery
publist_id: '271'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Race checking by context inference
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...