Date of Award
5-2017
Document Type
Thesis
Degree Name
Master of Science (MS)
Legacy Department
Computer Science
Committee Member
Dr. Murali Sitaraman, Committee Chair
Committee Member
Dr. Brian Dean
Committee Member
Dr. Feng Luo
Abstract
This thesis presents a non-trivial candidate software component assembly that presents an opportunity and a challenge to the progress towards automated verification. It presents an opportunity because the data abstraction implementation can serve as a proof of concept of the idea that well-designed and well-annotated software components with mathematical specifications and well-engineered implementation(s) lead to generated verification conditions (VCs) of correctness that are "obvious" to prove. It presents a challenge because verification of the implementation involves multiple theories and the use of a tree concept that is based on a general tree theory for which there are no special-purpose solvers. The thesis contains a specification for a conceptualization of a tree with a position that makes it easy to explore and navigate a tree even as it avoids any explicit references to simplify reasoning. The thesis also contains concept enhancements for trees and an implementation layered using trees for a data abstraction for searching (a version of maps). A key contribution is the development of the implementation so that it is amenable for verification with internal assertions such as representation invariants and abstraction relations, operation specifications, loop invariants, and progress metrics, all of which involve the general tree theory.
Recommended Citation
Mbwambo, Nicodemus M.J., "A Well-Designed, Tree-Based, Generic Map Component to Challenge the Progress towards Automated Verification" (2017). All Theses. 2657.
https://open.clemson.edu/all_theses/2657