Causality-based Model Checking

Bernd Finkbeiner
(Universität des Saarlandes)
Andrey Kupriyanov
(Institute of Science and Technology Austria)

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.

In Alex Groce and Stefan Leue: Proceedings 2nd International Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies (CREST 2017), Uppsala, Sweden, 29th April 2017, Electronic Proceedings in Theoretical Computer Science 259, pp. 31–38.
Published: 10th October 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: