Emma Tye, a 2nd year UROP student working with Philippa Garner and Jose Fragoso on JaVerT, presented her work at this year’s first group’s Wednesday meeting.
Emma’s UROP project focused on the specification and verification of AVL tree
algorithms and she managed to prove the most challenging algorithms ever
tackled using JaVerT. AVL trees are self-balanced binary search trees that are
difficult to understand and implement correctly. An AVL tree has various cases
in which it self-balances, each handled differently; therefore, well-crafted
abstractions are needed to achieve succinct readable specifications.
Emma used JaVerT to specify and mechanically verify several algorithms for AVL-tree operations, including insertion and removal of nodes, improving JaVerT in the process, by uncovering bugs and usability issues.