GPGPU Parallel SPIN Model Checker

Metadata Updated: May 2, 2019

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.

Access & Use Information

Public: This dataset is intended for public access and use. License: U.S. Government Work

Downloads & Resources


Metadata Created Date August 1, 2018
Metadata Updated Date May 2, 2019

Metadata Source

Harvested from NASA Data.json

Additional Metadata

Resource Type Dataset
Metadata Created Date August 1, 2018
Metadata Updated Date May 2, 2019
Publisher Space Technology Mission Directorate
Unique Identifier TECHPORT_11486
Maintainer Email
Public Access Level public
Bureau Code 026:00
Metadata Context
Metadata Catalog ID
Schema Version
Catalog Describedby
Datagov Dedupe Retained 20190501230127
Harvest Object Id 6c86d989-4559-4363-892c-1081eb3d4d6e
Harvest Source Id 39e4ad2a-47ca-4507-8258-852babd0fd99
Harvest Source Title NASA Data.json
Data First Published 2016-08-01
Homepage URL
Data Last Modified 2018-07-19
Program Code 026:027
Source Datajson Identifier True
Source Hash 47d3222538c406537f764f562937dae7a735a607
Source Schema Version 1.1

Didn't find what you're looking for? Suggest a dataset here.