A Non-Trivial Challenge Involving Trees for Automated Provers
Event Type
DescriptionThis paper 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 tree-based map 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 proving the VCs involves multiple theories and the use of a general tree theory written in higher-order logic for which there are no special-purpose solvers.