---
_id: '549'
abstract:
- lang: eng
  text: Model checking is usually based on a comprehensive traversal of the state
    space. Causality-based model checking is a radically different approach that instead
    analyzes the cause-effect relationships in a program. We give an overview on a
    new class of model checking algorithms that capture the causal relationships in
    a special data structure called concurrent traces. Concurrent traces identify
    key events in an execution history and link them through their cause-effect relationships.
    The model checker builds a tableau of concurrent traces, where the case splits
    represent different causal explanations of a hypothetical error. Causality-based
    model checking has been implemented in the ARCTOR tool, and applied to previously
    intractable multi-threaded benchmarks.
alternative_title:
- EPTCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Bernd
  full_name: Finkbeiner, Bernd
  last_name: Finkbeiner
- first_name: Andrey
  full_name: Kupriyanov, Andrey
  id: 2C311BF8-F248-11E8-B48F-1D18A9856A87
  last_name: Kupriyanov
citation:
  ama: 'Finkbeiner B, Kupriyanov A. Causality-based model checking. In: <i>Electronic
    Proceedings in Theoretical Computer Science</i>. Vol 259. Open Publishing Association;
    2017:31-38. doi:<a href="https://doi.org/10.4204/EPTCS.259.3">10.4204/EPTCS.259.3</a>'
  apa: 'Finkbeiner, B., &#38; Kupriyanov, A. (2017). Causality-based model checking.
    In <i>Electronic Proceedings in Theoretical Computer Science</i> (Vol. 259, pp.
    31–38). Uppsala, Sweden: Open Publishing Association. <a href="https://doi.org/10.4204/EPTCS.259.3">https://doi.org/10.4204/EPTCS.259.3</a>'
  chicago: Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.”
    In <i>Electronic Proceedings in Theoretical Computer Science</i>, 259:31–38. Open
    Publishing Association, 2017. <a href="https://doi.org/10.4204/EPTCS.259.3">https://doi.org/10.4204/EPTCS.259.3</a>.
  ieee: B. Finkbeiner and A. Kupriyanov, “Causality-based model checking,” in <i>Electronic
    Proceedings in Theoretical Computer Science</i>, Uppsala, Sweden, 2017, vol. 259,
    pp. 31–38.
  ista: 'Finkbeiner B, Kupriyanov A. 2017. Causality-based model checking. Electronic
    Proceedings in Theoretical Computer Science. CREST: Causal Reasoning for Embedded
    and Safety-Critical Systems Technologies, EPTCS, vol. 259, 31–38.'
  mla: Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.”
    <i>Electronic Proceedings in Theoretical Computer Science</i>, vol. 259, Open
    Publishing Association, 2017, pp. 31–38, doi:<a href="https://doi.org/10.4204/EPTCS.259.3">10.4204/EPTCS.259.3</a>.
  short: B. Finkbeiner, A. Kupriyanov, in:, Electronic Proceedings in Theoretical
    Computer Science, Open Publishing Association, 2017, pp. 31–38.
conference:
  end_date: 2017-04-29
  location: Uppsala, Sweden
  name: 'CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies'
  start_date: 2017-04-29
corr_author: '1'
date_created: 2018-12-11T11:47:07Z
date_published: 2017-10-10T00:00:00Z
date_updated: 2025-09-18T09:38:35Z
day: '10'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.4204/EPTCS.259.3
external_id:
  arxiv:
  - '1710.03391'
  isi:
  - '000439358700004'
file:
- access_level: open_access
  checksum: 6274f6c0da3376a7b079180d81568518
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:12:21Z
  date_updated: 2020-07-14T12:47:00Z
  file_id: '4939'
  file_name: IST-2018-925-v1+1_1710.03391v1.pdf
  file_size: 209294
  relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
intvolume: '       259'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1710.03391
month: '10'
oa: 1
oa_version: Submitted Version
page: 31 - 38
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
publication: Electronic Proceedings in Theoretical Computer Science
publication_identifier:
  issn:
  - 2075-2180
publication_status: published
publisher: Open Publishing Association
publist_id: '7264'
pubrep_id: '925'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Causality-based model checking
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 259
year: '2017'
...