Skip Navigation
Space Technology Research Grants

GPGPU Parallel SPIN Model Checker

Completed Technology Project

Project Description

Project Image   GPGPU Parallel SPIN Model Checker

Model Checking is a powerful technique used to verify that a system does not violate its intended behavior. While this is very useful in proving the robustness of a system, one drawback is that as the system grows in complexity or the number of properties being checked increases the time it takes to complete the model checking process grows exponentially larger. General-Purpose computing on Graphics Processor (GPGPU) architecture allows for programs to be rapidly executed on thousands of threads as a cheap alternative to supercomputing clusters. The goal of this project is to utilize CUDA and OpenCL GPGPU frameworks in order to parallelize the SPIN model checker to the greatest extent possible.

More »

Anticipated Benefits

Project Library

Primary U.S. Work Locations and Key Partners

Technology Transitions

Light bulb

Suggest an Edit

Recommend changes and additions to this project record.