Today I talked at the SPIN 2014 symposium in San Jose, CA about the SpinCause tool. The slides for my talk are available here.
In this paper we present the SpinCause tool for causality checking of Promela and PRISM models. We give an overview of the capabilities of SpinCause and briefly sketch how the causality checking algorithms are integrated into the state-space exploration algorithms used for model checking. In addition we compare the runtime and memory needed for causality checking with the different state-space exploration algorithms and two newly proposed iterative causality checking approaches.