STONY BROOK, NY, May 18, 2012 

This prestigous award is presented to students based upon three criteria: the merit of the proposed research, how well the project align's with NASA's goals, and the academic excellence of the student.

According to Dr. Michael J. Gazarik, the NASA Space Technology Program Director, "[b]eing selected as a NASA Space Technology Research Fellow is a real mark of distinction."

Richard was selected for his proposed project of a Graphics Processing Unit (GPU) based parallel version of the SPIN model checker. He began contributing to the project last summer in coordination with Dr. Ed Gamble of the Laboratory for Reliable Software (LaRS) at NASA's Jet Propulsion Laboratory (JPL). The continued effort has the enthusiastic support of Dr. Gerard Holzmann, the leader of LaRS and developer of the original SPIN model checker. Dr. Holzmann has been in communication with Richard's advisor, Professor Scott Smolka, about the fellowship. He has already expressed interest in having Richard spend a portion of the summer at JPL in Pasadena to work on the project. Richard's fellowship requires, and funds, up to ten weeks on-site at a NASA research laboratory during the one year fellowship period.

Model checking is a powerful technique used to verify correctness and safety properties of large hardware and software systems. Discovering potential errors through the use of model checkers such as SPIN can potentially save millions of dollars, and in the case of NASA missions, prevent critical mission failures. Unfortunately, as a system grows in complexity model checking suffers from state space explosion- an exponential growth in the number of states to be checked. This often results in either an over-simplification of some elements of the model or only a partial exploration of the state space. These practices allow for many potential errors to remain hidden, which could prove costly if they come up after the system has been deployed.

The advent of GPU-based parallel architectures such as Nvidia's Compute Unified Device Architecture (CUDA) and the Open Computing Language (OpenCL) has allowed for supercomputer level performance to be available in consumer grade computer systems. Although programs must be rewritten to make efficient use of the parallelism offered by graphics processors, the payoff is often on the level of three orders of magnitude in speedup. In the case of model checking, this could translate to one thousand times the state space exploration and discovery of potential errors.

In addition to the distinction and experience offered by the fellowship program, Richard will receive a stipend of $36,000 for the year as well as full payment of his tution and fees at Stony Brook. His on-site NASA research lab experience at JPL is covered by another $10,000 and up to $9,000 is available for conference and workshop expenses. Finally, he will receive a $1000 health insurance allowance for the year.

Richard is a member of the Concurrency and Verification (CaV) Lab located in both the CS and Center of Excellence in Wireless and Information Technology (CEWIT) buildings. The lab is led by Professor Scott Smolka and Professor Radu Grosu. Current lab projects include towers of abstraction for sodium ion flow models of cardiac myocytes, Hybrid Automata based feedback controllers, and analysis of spiral break-up in cardiac arrythmia. Much of the lab's work is funded by a National Science Foundation (NSF) grant to the Computational Modeling and Analysis for Complex Systems (CMACS) program.