Scalable Model Checking Using Compiler Analyses and the Alef SAT Solver
Agency / Branch:
DOD / OSD
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.
Small Business Information at Submission:
RESERVOIR LABS., INC.
632 Broadway, Suite 803 New York, NY 10012
Number of Employees: