Skip to main content.


CUDA Accelerated LTL Model Checker

DiVinE CUDA is an extensible open source tool for formal verification of concurrent systems. DiVinE CUDA is a standalone verification tool that supplements DiVinE verification tool chain with CUDA accelerated LTL model checking ability.

DiVinE CUDA builds upon MAP algorithm reformulated in terms of repeated matrix-vector product. The tool first generate state space of the model under inspection, stores it in a form of a matrix, and then employs CUDA architecture to solve the accepting cycle detection problem on the graph represented with the matrix.

Download and install instruction


Install instructions:

Using the tool