Skip Navigation
Space Technology Research Grants

GPGPU Parallel SPIN Model Checker

Active Technology Project

Project Introduction

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

Primary U.S. Work Locations and Key Partners

Share this Project

Organizational Responsibility

Project Management

Project Duration

Technology Maturity (TRL)

Technology Areas

^