Date of Award
Doctor of Philosophy (PhD)
Hallstrom , Jason
Krone , Joan
Jacobs , David
The foundational goal of this work is the development of mechanizable proof rules and a verification condition generator based on those rules for modern software. The verification system will be modular so that it is possible to verify the implementation of a component relying upon only the specifications of underlying components that are reused. The system must enable full behavioral verification. The proof rules used to generate verification conditions (VCs) of correctness must be amenable to automation. While automation requires software developers to annotate implementations with assertions, it should not require assistance in the proofs. This research has led to a VC generator that realizes these goals. The VC generator has been applied to a range of benchmarks to show the viability of verified components. It has been used in classrooms at multiple institutions to teach reasoning principles.
A fundamental problem in computing is the inability to show that a software system behaves as required. Modern software systems are composed of numerous software components. The fundamental goal of this work is to verify each independently in a modular fashion, resulting in full behavioral verification and providing an assurance that components meet their specifications and can be used with confidence to build verified software systems. Of course, to be practical, such a system must be mechanical. Although the principles of verification have existed for decades, the basis for a practical verification system for modern software components has remained elusive.
Harton, Heather, "Mechanical and Modular Verification Condition Generation for Object-Based Software" (2011). All Dissertations. 869.