GPU explicit-state model checkingThe GPUexplore tool (version 2.0) can be used to perform explicit state space exploration and on-the-fly model checking of deadlocks and safety properties completely on an NVIDIA GPU with at least CUDA computation capability 3.0. State space exploration is the basis on which explicit-state model checking procedures rely. Download links for both the tool and a set of models for experimentation are provided on this page. To explore the state spaces of those models directly on a CPU, the model checking toolsets mCRL2 and CADP are required.
REQUIRED PACKAGES: CUDA driver + SDK; to produce GPU encodings of the models, and to generate the state spaces on a CPU: Python, CADP, and mCRL2