@inproceedings{549, 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.}, author = {Finkbeiner, Bernd and Kupriyanov, Andrey}, booktitle = {Electronic Proceedings in Theoretical Computer Science}, issn = {2075-2180}, location = {Uppsala, Sweden}, pages = {31 -- 38}, publisher = {Open Publishing Association}, title = {{Causality-based model checking}}, doi = {10.4204/EPTCS.259.3}, volume = {259}, year = {2017}, }