Date of Award
Master of Science (MS)
Dr. Murali Sitaraman, Committee Chair
Dr. Brian Dean
Dr. Feng Luo
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.
Mbwambo, Nicodemus M.J., "A Well-Designed, Tree-Based, Generic Map Component to Challenge the Progress towards Automated Verification" (2017). All Theses. 2657.