Date of Award
12-2011
Document Type
Dissertation
Degree Name
Doctor of Philosophy (PhD)
Legacy Department
Computer Science
Committee Chair/Advisor
Sitaraman, Murali
Committee Member
Hallstrom , Jason
Committee Member
Krone , Joan
Committee Member
Jacobs , David
Abstract
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.
Recommended Citation
Harton, Heather, "Mechanical and Modular Verification Condition Generation for Object-Based Software" (2011). All Dissertations. 869.
https://tigerprints.clemson.edu/all_dissertations/869