Date of Award

12-2018

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Committee Member

Murali Sitaraman, Committee Chair

Committee Member

John D McGregor

Committee Member

Nigamanth Sridhar

Committee Member

Pradip K Srimani

Abstract

Automated verification is critical for ensuring that an implementation is correct and meets the specified behavior on every valid input. Verification should be modular to promote reuse and to scale up. However, for code that involves explicit reference behavior, there is the added complexity of reasoning that only the intended objects are being affected. This research focuses on simplifying automated verification and enabling modular verification using data abstractions that hide explicit reference behavior. While avoiding explicit reference behavior simplifies reasoning for a majority of software components, for capturing unavoidable reference behavior, such as that needed to implement classes of lower-level "linked" realizations such as for lists and trees, the research introduces and uses automation-friendly abstractions to capture acyclic reference behavior. The overall research involves the development of specification and verification mechanisms for components where objects share a global state, along with a new prototype verification system that is designed to generate simplified verification conditions with automation in mind. Experimentation and evaluation involve a class of components with and without explicit reference behavior.

Share

COinS