Add new file

_posts/2018-10-10-emma.md

+---
+title: Talk by Emma Tye, UROP student with the group, AVL tree algorithms
+---
+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.
\ No newline at end of file