@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},
}