Causality-based model checking

B. Finkbeiner, A. Kupriyanov, in:, Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, 2017, pp. 31–38.

Download
OA 209.29 KB

Conference Paper | Published | English
Author
;
Department
Series Title
EPTCS
Abstract
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.
Publishing Year
Date Published
2017-10-10
Proceedings Title
Electronic Proceedings in Theoretical Computer Science
Volume
259
Page
31 - 38
Conference
CREST: Causal Reasoning for Embedded and Safety-Critical Systems Technologies
Conference Location
Uppsala, Sweden
Conference Date
2017-04-29 – 2017-04-29
ISSN
IST-REx-ID

Cite this

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
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
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.
B. Finkbeiner and A. Kupriyanov, “Causality-based model checking,” in Electronic Proceedings in Theoretical Computer Science, Uppsala, Sweden, 2017, vol. 259, pp. 31–38.
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.
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.
Main File(s)
Access Level
OA Open Access
Last Uploaded
2018-12-12T10:12:21Z


Link(s) to Main File(s)
Access Level
OA Open Access

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar