|
GPU explicit-state model checking
The 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
|
The GPUexplore source code.
|
DOWNLOAD
INSTRUCTIONS |
Experimental data (set of input models)
(When using Safari, open in New Window or Tab).
|
DOWNLOAD
|
|
