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

Posted on


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.

About GrammaTech:
GrammaTech’s static-analysis tools are used worldwide by startups, Fortune 500 companies, educational institutions, and government agencies. The staff includes fourteen researchers with PhDs in programming languages and program analysis.

Book a Demo

We’re ready to help you integrate SAST and SCA security into your DevSecOps flow. Get a personally guided tour of our solution offerings to ensure you are receiving the right solution for your development team. 

book now