Richard DeFrancisco is awarded 2012 NASA fellowship

Computer Science PhD student Richard DeFrancisco of Stony Brook University has been awarded a 2012 National Aeronautics and Space Administration (NASA) Space Technology Research Fellowship (NSTRF).
His project is the development of a Graphics Processing Unit (GPU) based parallel version of the SPIN model checker. The award, in the amount of $63,617 for a period of one year, includes expenses for tuition and fees, health insurance, conference attendance, journal publication, a healthy stipend, and a 10-week experience at a NASA facility.

Richard has been partnered with CMACS member Dr. Gerard Holzmann of NASA JPL's Laboratory for Reliable Software (LaRS), developer of the SPIN model checker.  Dr. Holzmann will serve as his official NASA mentor  and will host Richard's 10-week experience at his JPL lab.
The on-site visit will be used to further develop and refine the software system, which is already being designed.

The project goal is to utilize Nvidia's Compute Unified Device Architecture (CUDA) to massively parallelize the SPIN model checker, increasing its speed by orders of magnitude.  This will allow large systems to be modeled in much greater detail and checked in the same amount of time as a more simplified model being checked with classical SPIN.  While Dr. Holzmann has already made great strides in adding smaller-scale parallelism to the model checker, and the theory is still applicable, major alterations to the algorithms will be necessary to facilitate the intricacies of the GPU architecture.

For more information about this project, please visit http://www.nasa.gov/offices/oct/early_stage_innovation/grants/2012_nstrf_defrancisco.html.