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.