Date of Award


Document Type


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


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.



To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.