---
_id: '4463'
abstract:
- lang: eng
  text: We present an algorithm called TAR (“Thread-modular Abstraction Refinement”)
    for model checking safety properties of concurrent software. The TAR algorithm
    uses thread-modular assume-guarantee reasoning to overcome the exponential complexity
    in the control state of multithreaded programs. Thread modularity means that TAR
    explores the state space of one thread at a time, making assumptions about how
    the environment can interfere. The TAR algorithm uses counterexample-guided predicate-abstraction
    refinement to overcome the usually infinite complexity in the data state of C
    programs. A successive approximation scheme automatically infers the necessary
    precision on data variables as well as suitable environment assumptions. The scheme
    is novel in that transition relations are approximated from above, while at the
    same time environment assumptions are approximated from below. In our software
    verification tool BLAST we have implemented a fully automatic race checker for
    multithreaded C programs which is based on the TAR algorithm. This tool has verified
    a wide variety of commonly used locking idioms, including locking schemes that
    are not amenable to existing dynamic and static race checkers such as ERASER or
    WARLOCK.
acknowledgement: This work was supported in part by the NSF grants CCR-0085949 and
  CCR-0234690, the DARPA grant F33615-00-C-1693, and the MARCO grant 98-DT-660.
alternative_title:
- LNCS
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
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
citation:
  ama: 'Henzinger TA, Jhala R, Majumdar R, Qadeer S. Thread-modular abstraction refinement.
    In: <i>Proceedings of the 15th International Conference on Computer Aided Verification</i>.
    Vol 2725. Springer; 2003:262-274. doi:<a href="https://doi.org/10.1007/978-3-540-45069-6_27">10.1007/978-3-540-45069-6_27</a>'
  apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Qadeer, S. (2003). Thread-modular
    abstraction refinement. In <i>Proceedings of the 15th International Conference
    on Computer Aided Verification</i> (Vol. 2725, pp. 262–274). Boulder, CO, USA:
    Springer. <a href="https://doi.org/10.1007/978-3-540-45069-6_27">https://doi.org/10.1007/978-3-540-45069-6_27</a>'
  chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Shaz Qadeer.
    “Thread-Modular Abstraction Refinement.” In <i>Proceedings of the 15th International
    Conference on Computer Aided Verification</i>, 2725:262–74. Springer, 2003. <a
    href="https://doi.org/10.1007/978-3-540-45069-6_27">https://doi.org/10.1007/978-3-540-45069-6_27</a>.
  ieee: T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer, “Thread-modular abstraction
    refinement,” in <i>Proceedings of the 15th International Conference on Computer
    Aided Verification</i>, Boulder, CO, USA, 2003, vol. 2725, pp. 262–274.
  ista: 'Henzinger TA, Jhala R, Majumdar R, Qadeer S. 2003. Thread-modular abstraction
    refinement. Proceedings of the 15th International Conference on Computer Aided
    Verification. CAV: Computer Aided Verification, LNCS, vol. 2725, 262–274.'
  mla: Henzinger, Thomas A., et al. “Thread-Modular Abstraction Refinement.” <i>Proceedings
    of the 15th International Conference on Computer Aided Verification</i>, vol.
    2725, Springer, 2003, pp. 262–74, doi:<a href="https://doi.org/10.1007/978-3-540-45069-6_27">10.1007/978-3-540-45069-6_27</a>.
  short: T.A. Henzinger, R. Jhala, R. Majumdar, S. Qadeer, in:, Proceedings of the
    15th International Conference on Computer Aided Verification, Springer, 2003,
    pp. 262–274.
conference:
  end_date: 2003-07-12
  location: Boulder, CO, USA
  name: 'CAV: Computer Aided Verification'
  start_date: 2003-07-08
date_created: 2018-12-11T12:08:59Z
date_published: 2003-06-27T00:00:00Z
date_updated: 2024-01-10T11:05:53Z
day: '27'
doi: 10.1007/978-3-540-45069-6_27
extern: '1'
intvolume: '      2725'
language:
- iso: eng
month: '06'
oa_version: None
page: 262 - 274
publication: Proceedings of the 15th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540405245'
publication_status: published
publisher: Springer
publist_id: '266'
quality_controlled: '1'
status: public
title: Thread-modular abstraction refinement
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2725
year: '2003'
...