Causality-based Model Checking

TL;DR

Causality-based model checking analyzes cause-effect relationships in programs using concurrent traces, offering a novel approach that can handle complex multi-threaded systems more effectively than traditional state space traversal methods.

Contribution

This paper introduces a new causality-based model checking algorithm utilizing concurrent traces, enabling analysis of complex multi-threaded programs and overcoming limitations of traditional methods.

Findings

Successfully applied to intractable multi-threaded benchmarks

Implemented in the ARCTOR tool

Captures causal relationships for error explanation

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.