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.
Recommended Citation
Sun, Yu-Shan, "Towards Automated Verification of Object-Based Software with Reference Behavior" (2018). All Dissertations. 2280.
https://open.clemson.edu/all_dissertations/2280