---
_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
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
date_created: 2018-12-11T11:47:07Z
date_published: 2017-10-10T00:00:00Z
date_updated: 2023-10-17T12:02:46Z
day: '10'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.4204/EPTCS.259.3
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'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1710.03391v1
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: The Wittgenstein Prize
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 259
year: '2017'
...
---
_id: '1391'
abstract:
- lang: eng
  text: "We present an extension to the quantifier-free theory of integer arrays which
    allows us to express counting. The properties expressible in Array Folds Logic
    (AFL) include statements such as &quot;the first array cell contains the array
    length,&quot; and &quot;the array contains equally many minimal and maximal elements.&quot;
    These properties cannot be expressed in quantified fragments of the theory of
    arrays, nor in the theory of concatenation. Using reduction to counter machines,
    we show that the satisfiability problem of AFL is PSPACE-complete, and with a
    natural restriction the complexity decreases to NP. We also show that adding either
    universal quantifiers or concatenation leads to undecidability.\r\nAFL contains
    terms that fold a function over an array. We demonstrate that folding, a well-known
    concept from functional languages, allows us to concisely summarize loops that
    count over arrays, which occurs frequently in real-life programs. We provide a
    tool that can discharge proof obligations in AFL, and we demonstrate on practical
    examples that our decision procedure can solve a broad range of problems in symbolic
    testing and program verification."
alternative_title:
- LNCS
author:
- first_name: Przemyslaw
  full_name: Daca, Przemyslaw
  id: 49351290-F248-11E8-B48F-1D18A9856A87
  last_name: Daca
- 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: Andrey
  full_name: Kupriyanov, Andrey
  id: 2C311BF8-F248-11E8-B48F-1D18A9856A87
  last_name: Kupriyanov
citation:
  ama: 'Daca P, Henzinger TA, Kupriyanov A. Array folds logic. In: Vol 9780. Springer;
    2016:230-248. doi:<a href="https://doi.org/10.1007/978-3-319-41540-6_13">10.1007/978-3-319-41540-6_13</a>'
  apa: 'Daca, P., Henzinger, T. A., &#38; Kupriyanov, A. (2016). Array folds logic
    (Vol. 9780, pp. 230–248). Presented at the CAV: Computer Aided Verification, Toronto,
    Canada: Springer. <a href="https://doi.org/10.1007/978-3-319-41540-6_13">https://doi.org/10.1007/978-3-319-41540-6_13</a>'
  chicago: Daca, Przemyslaw, Thomas A Henzinger, and Andrey Kupriyanov. “Array Folds
    Logic,” 9780:230–48. Springer, 2016. <a href="https://doi.org/10.1007/978-3-319-41540-6_13">https://doi.org/10.1007/978-3-319-41540-6_13</a>.
  ieee: 'P. Daca, T. A. Henzinger, and A. Kupriyanov, “Array folds logic,” presented
    at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9780, pp.
    230–248.'
  ista: 'Daca P, Henzinger TA, Kupriyanov A. 2016. Array folds logic. CAV: Computer
    Aided Verification, LNCS, vol. 9780, 230–248.'
  mla: Daca, Przemyslaw, et al. <i>Array Folds Logic</i>. Vol. 9780, Springer, 2016,
    pp. 230–48, doi:<a href="https://doi.org/10.1007/978-3-319-41540-6_13">10.1007/978-3-319-41540-6_13</a>.
  short: P. Daca, T.A. Henzinger, A. Kupriyanov, in:, Springer, 2016, pp. 230–248.
conference:
  end_date: 2016-07-23
  location: Toronto, Canada
  name: 'CAV: Computer Aided Verification'
  start_date: 2016-07-17
date_created: 2018-12-11T11:51:45Z
date_published: 2016-07-13T00:00:00Z
date_updated: 2023-09-07T11:58:33Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-319-41540-6_13
ec_funded: 1
intvolume: '      9780'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1603.06850
month: '07'
oa: 1
oa_version: Preprint
page: 230 - 248
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication_status: published
publisher: Springer
publist_id: '5818'
quality_controlled: '1'
related_material:
  record:
  - id: '1155'
    relation: dissertation_contains
    status: public
scopus_import: 1
status: public
title: Array folds logic
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9780
year: '2016'
...