Scalable Parallel Algorithms for Formal Verification of Software

Award Information
Agency:
National Aeronautics and Space Administration
Branch
n/a
Amount:
$125,000.00
Award Year:
2012
Program:
SBIR
Phase:
Phase I
Contract:
NNX12CD03P
Award Id:
n/a
Agency Tracking Number:
115077
Solicitation Year:
2011
Solicitation Topic Code:
A1.20
Solicitation Number:
n/a
Small Business Information
IL, Chicago, IL, 60618-3745
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
361627933
Principal Investigator:
Miroslav Velev
Principal Investigator
(773) 856-6633
miroslav.velev@aries-da.com
Business Contact:
Miroslav Velev
Business Official
(773) 856-6633
miroslav.velev@aries-da.com
Research Institute:
Stub




Abstract
We will develop a prototype of a GPU-based parallel Binary Decision Diagram (BDD) software package. 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 graphics processors (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 a BDD package, and to explore hybrid approaches that will combine this GPU-based BDD package with our GPU-based parallel SAT solver that we are currently developing in a NASA SBIR Phase II project. The goal will be to achieve increased speed, as well as scalability for much larger state spaces when formally verifying complex software for space applications. We anticipate increase in both speed and scalability by 1?2 orders of magnitude by the end of Phase I, and 3?4 orders of magnitude by the end of Phase II, compared to the current approaches.

* information listed above is at the time of submission.

Agency Micro-sites


SBA logo

Department of Agriculture logo

Department of Commerce logo

Department of Defense logo

Department of Education logo

Department of Energy logo

Department of Health and Human Services logo

Department of Homeland Security logo

Department of Transportation logo

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government