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