diff --git a/_posts/2018-10-10-emma.md b/_posts/2018-10-10-emma.md new file mode 100644 index 0000000000000000000000000000000000000000..45d1b9e266c8a1dff180e1f26a0390e900c1b6ca --- /dev/null +++ b/_posts/2018-10-10-emma.md @@ -0,0 +1,15 @@ +--- +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