2018-10-10-emma.md

---
title: Talk by Emma Tye, UROP student with the group, AVL tree algorithms
---
[Emma Tye](https://github.com/EmmaTye), 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.