--- _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' ... --- _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 "the first array cell contains the array length," and "the array contains equally many minimal and maximal elements." 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:10.1007/978-3-319-41540-6_13' apa: 'Daca, P., Henzinger, T. A., & Kupriyanov, A. (2016). Array folds logic (Vol. 9780, pp. 230–248). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. https://doi.org/10.1007/978-3-319-41540-6_13' chicago: Daca, Przemyslaw, Thomas A Henzinger, and Andrey Kupriyanov. “Array Folds Logic,” 9780:230–48. Springer, 2016. https://doi.org/10.1007/978-3-319-41540-6_13. 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. Array Folds Logic. Vol. 9780, Springer, 2016, pp. 230–48, doi:10.1007/978-3-319-41540-6_13. 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' ...