Scalable Model Checking Using Compiler Analyses and the Alef SAT Solver

Award Information
Agency:
Department of Defense
Amount:
$99,940.00
Program:
SBIR
Contract:
W911QX-06-C-0099
Solitcitation Year:
2005
Solicitation Number:
2005.3
Branch:
Army
Award Year:
2006
Phase:
Phase I
Agency Tracking Number:
O053-SP5-2076
Solicitation Topic Code:
OSD05-SP5
Small Business Information
RESERVOIR LABS., INC.
632 Broadway, Suite 803, New York, NY, 10012
Hubzone Owned:
N
Woman Owned:
N
Socially and Economically Disadvantaged:
N
Duns:
022423854
Principal Investigator
 Eric Schweitz
 Managing Engineer
 (212) 780-0527
 schweitz@reservoir.com
Business Contact
 Melanie Peters
Title: Business Manager
Phone: (212) 780-0527
Email: peters@reservoir.com
Research Institution
N/A
Abstract
Our objective is to produce a commercial-grade model checking system that is scalable, end-to-end and highly usable. By scalable, we mean that the system will check larger software systems and answer more detailed queries than existing systems. By end-to-end, we mean that the system will automate the entire model-checking process from the point where the developer submits a query to the point where results are presented to the developer. By highly usable, we mean that the developer will not be required to learn any special-purpose modeling or specification languages in order to make full use of the system.

* information listed above is at the time of submission.

Agency Micro-sites

US Flag An Official Website of the United States Government