USA flag logo/image

An Official Website of the United States Government

Verification of Hierarchical Graph Structures

Award Information

Department of Defense
Defense Advanced Research Projects Agency
Award ID:
Program Year/Program:
2002 / SBIR
Agency Tracking Number:
Solicitation Year:
Solicitation Topic Code:
Solicitation Number:
Small Business Information
GrammaTech, Inc
531 Esty Street Ithaca, NY -
View profile »
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
Phase 2
Fiscal Year: 2002
Title: Verification of Hierarchical Graph Structures
Agency / Branch: DOD / DARPA
Contract: DAAH01-02-C-R120
Award Amount: $381,099.00


"The security and prosperity of the nation has become increasingly dependent on complex software systems. Unfortunately, current practice usually yields software that is generally unreliable and insecure. The industry must reduce reliance on methods thatcan only detect the presence of faults, and move towards methods that can demonstrate their absence. Model checking is a verification technique that allows users to verify crosscutting properties of systems. During Phase I of this project, we developed anew technique for model checking based on using context-free-language reachability algorithms. These allow us to exploit the inherent modularity in procedural abstraction, and thus allow the technique to be scaled to large programs. We constructed aprototype of a system and demonstrated how it can be used to find real faults in software. We investigated methods for using our dependence graph and program slicing technology to construct models of a reduced size so as to further improve the scalabilityof the system. In Phase II, we propose to build on our Phase I results and create a product capable of being applied to industrial-sized problems. Initial evidence suggests great potential benefits. Our commercialization strategy will ensure rapidexploitation and early success in Phase III."

Principal Investigator:

Paul Anderson
Senior Software Engineer

Business Contact:

Ray Teitelbaum
Small Business Information at Submission:

Grammatech, Inc.
317 N. Aurora Street Ithaca, NY 14850

EIN/Tax ID: 161338879
Number of Employees:
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No