--- _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: Electronic Proceedings in Theoretical Computer Science. Vol 259. Open Publishing Association; 2017:31-38. doi:10.4204/EPTCS.259.3' apa: 'Finkbeiner, B., & Kupriyanov, A. (2017). Causality-based model checking. In Electronic Proceedings in Theoretical Computer Science (Vol. 259, pp. 31–38). Uppsala, Sweden: Open Publishing Association. https://doi.org/10.4204/EPTCS.259.3' chicago: Finkbeiner, Bernd, and Andrey Kupriyanov. “Causality-Based Model Checking.” In Electronic Proceedings in Theoretical Computer Science, 259:31–38. Open Publishing Association, 2017. https://doi.org/10.4204/EPTCS.259.3. ieee: B. Finkbeiner and A. Kupriyanov, “Causality-based model checking,” in Electronic Proceedings in Theoretical Computer Science, 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.” Electronic Proceedings in Theoretical Computer Science, vol. 259, Open Publishing Association, 2017, pp. 31–38, doi:10.4204/EPTCS.259.3. 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' ...