From 963a280ce3e6a65b6237faac7278d675042838cd Mon Sep 17 00:00:00 2001
From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk>
Date: Wed, 7 Nov 2018 15:23:59 +0000
Subject: [PATCH] Add new file

---
 _posts/2018-10-10-emma.md | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 _posts/2018-10-10-emma.md

diff --git a/_posts/2018-10-10-emma.md b/_posts/2018-10-10-emma.md
new file mode 100644
index 0000000..45d1b9e
--- /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
-- 
GitLab