Verification of Hierarchical Graph Structures

"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."