GrammaTech Awarded DARPA Phase II SBIR Research Contract to Develop Techniques for Model Checking Hierarchical Graph Structures

Ithaca, NY — GrammaTech, Inc. announced today that it has been awarded a two-year $749,118 Small Business Innovative Research (SBIR) Phase II contract by the Defense Advanced Research Projects Agency (DARPA). Under the terms of the contract, GrammaTech will develop a model checker for C/C++ software. Model Checking is a technique for verifying properties of software, using exhaustive exploration of all possible program executions. This technology is of obvious interest in projects in which high-assurance concerns are paramount, such as air-traffic control systems, military systems, and medical systems.

Under current practice, the quality of software systems is typically assessed using a time-consuming and costly testing process. Unfortunately, this process can only detect the presence of faults, and can never show their absence; so most systems are deployed with bugs lurking deep in unexplored crevices of the code. The software makers expect that these faults will show up in the field, and are usually prepared to issue fixes reactively. While this may be acceptable for, say, a word processor, it is clearly not so for real-time software that controls life-critical or mission-critical systems. Model checking is a technique that can verify the absence of a particular fault in software.

The Phase II contract represents an expansion of an earlier $98,941 Phase I project that DARPA funded to explore the technical feasibility of GrammaTech’s approach. During the Phase I effort GrammaTech developed a prototype model checker that works for moderate sized C programs. Under the DARPA Phase II contract, GrammaTech produce an model checking based automated fault-detection tool that statically finds flaws in C/C++ programs. The tool will be able to detect both generic-programming flaws, as well as verify domain-specific properties of a software system.