Date of Award

12-2011

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Legacy Department

Computer Science

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.

Share

COinS