NASA SBIR 2008 Solicitation

FORM B - PROPOSAL SUMMARY


PROPOSAL NUMBER: 08-1 X1.02-8609
SUBTOPIC TITLE: Reliable Software for Exploration Systems
PROPOSAL TITLE: An Efficient Parallel SAT Solver Exploiting Multi-Core Environments

SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
Aries Design Automation, LLC
6157 N Sheridan Road, Suite 16M
Chicago, IL 60660 - 5818
(773) 856-6633

PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
Miroslav Velev
miroslav.velev@aries-da.com
6157 N Sheridan Road, Suite 16M
Chicago, IL 60660 - 5818
(773) 856-6633

Expected Technology Readiness Level (TRL) upon completion of contract: 5 to 6

TECHNICAL ABSTRACT (Limit 2000 characters, approximately 200 words)
The hundreds of stream cores in the latest graphics processors (GPUs), and the possibility to execute non-graphics computations on them, open unprecedented levels of parallelism at a very low cost. We will investigate ways to efficiently exploit this parallelism in order to accelerate the execution of a Boolean Satisfiability (SAT) solver. SAT has a wide range of applications, including formal verification and testing of software and hardware, scheduling and planning, cryptanalysis, and detection of security vulnerabilities and malicious intent. We bring a tremendous expertise in SAT solving, formal verification, and solving of Constraint Satisfaction Problems (CSPs) by efficient translation to SAT. In our previous work (done on the expenses of our company) we obtained 2 orders of magnitude speedup in solving Boolean formulas from formal verification of complex pipelined microprocessors, as well as 4 orders of magnitude speedup in SAT-based solving of CSPs. We expect to achieve speedups of up to 1 – 2 orders of magnitude in Phase 1, and up to 3 – 4 orders of magnitude in Phase 2.

POTENTIAL NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
Efficiently solving of challenging Boolean formulas is critical to NASA, as this will increase both the scalability and speed of formal verification and testing methods for complex mission software and hardware, as well as of SAT-based methods for solving of scheduling and planning problems.

POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
The potential non-NASA commercial applications include:
1) Formal verification and testing of software and hardware, where the potential customers will be all major semiconductor and software companies.
2) Scheduling, planning, and solving of Constraint Satisfaction Problems (CSPs), where the potential customers will be all companies that develop scheduling and planning tools.
3) Formal methods for cryptanalysis, where the potential customers will be the Department of Defense, the NSA, and all companies that use cryptanalysis.
4) Formal methods for cyber security, such as for detection of security vulnerabilities and malicious intent in software, where the potential customers will be all companies that develop robust virus scanners based on formal methods, and companies that develop formal methods for detecting security vulnerabilities in software. Because of the potential for a very wide range of software obfuscations that can be used to hide malicious intent, future virus scanners will have to employ efficient formal methods to detect malware, and thus the importance of speed and scalability that will be possible due to an efficient SAT solver.

NASA's technology taxonomy has been developed by the SBIR-STTR program to disseminate awareness of proposed and awarded R/R&D in the agency. It is a listing of over 100 technologies, sorted into broad categories, of interest to NASA.

TECHNOLOGY TAXONOMY MAPPING
Architectures and Networks
Autonomous Reasoning/Artificial Intelligence
Computer System Architectures
Data Input/Output Devices
Expert Systems
Highly-Reconfigurable
Intelligence
Operations Concepts and Requirements
Simulation Modeling Environment
Software Development Environments
Software Tools for Distributed Analysis and Simulation
Testing Facilities
Testing Requirements and Architectures
Training Concepts and Architectures


Form Generated on 11-24-08 11:56