You are here

Scalable Parallel Algorithms for Formal Verification of Software

Award Information
Agency: National Aeronautics and Space Administration
Branch: N/A
Contract: NNX13CL52P
Agency Tracking Number: 125314
Amount: $125,000.00
Phase: Phase I
Program: SBIR
Solicitation Topic Code: A1.06
Solicitation Number: N/A
Solicitation Year: 2012
Award Year: 2013
Award Start Date (Proposal Award Date): 2013-05-23
Award End Date (Contract End Date): 2013-11-23
Small Business Information
IL, Chicago, IL, 60618-3745
DUNS: 361627933
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 Miroslav Velev
 Principal Investigator
 (773) 856-6633
Business Contact
 Miroslav Velev
Title: Business Official
Phone: (773) 856-6633
Research Institution
We will develop an efficient Graphics Processing Unit (GPU) based parallel Binary Decision Diagram (BDD) software package, and will also combine it with our GPU-based parallel SAT solver that we are currently developing in a NASA SBIR Phase II project in order to solve much larger and more complex Boolean formulas from formal verification than possible with either method alone. BDDs are a data structure that satisfies some simple restrictions, resulting in a unique representation of a Boolean function regardless of its actual implementation. This property of BDDs allows the efficient solution of many problems. The proposed tool will exploit multi-core CPUs and the thousands of stream cores in the latest GPUs, which were made accessible to programmers through specialized software development kits. These large numbers of stream cores in GPUs, and the possibility to execute non-graphics computations on them, open unprecedented levels of parallelism at a very low cost. In the last 8 years, GPUs had an increasing performance advantage of an order of magnitude relative to x86 CPUs. Furthermore, this performance advantage will continue to increase in the next 20 years because of the scalability of the chip manufacturing processes. The technical objectives will be to efficiently exploit the GPU parallelism in order to accelerate the execution of our prototype GPU-based parallel BDD package, and to implement hybrid approaches combining it with our GPU-based parallel SAT solver. BDDs and SAT solvers are orthogonal methods with different advantages, and a hybrid of the two will significantly increase both the speed and capacity when formally verifying complex software for space missions. We achieved at least 2 orders of magnitude speedup with our prototype GPU-based parallel BDD package in a previous Phase I, and expect to achieve at least 4 orders of magnitude speedup with our hybrid BDD-SAT tool by the end of Phase II, compared to the current state of the art.

* Information listed above is at the time of submission. *

US Flag An Official Website of the United States Government