Merge remote-tracking branch 'origin/master'

# Conflicts:
#	_posts/2020-07-08-aalwines.md

Author: tfenz

_posts/2020-06-24-aalwines.md _posts/2020-07-08-aalwines.md_posts/2020-06-24-aalwines.md renamed to _posts/2020-07-08-aalwines.md

@@ -89,22 +89,24 @@ The configurations are put into a standardized, intermediate format which is ven
 The user can then define a query as described above, which leads the tool to prompt with a result 
 (e.g. a trace). AalWiNes is a joint work at Aalborg University and the University of Vienna.
 
-For MPLS specifically, we have developed the AalWiNes tool, implemented in C++.
+For MPLS specifically, we have devloped the AalWiNes tool suite, implemented in C++, and improving upon an earlier
+prototype implementation in Python [[1]](#references).
 The tool allows to verify a wide range of important network properties in polynomial time, 
 parameterized by the $k$. 
-Here is a quick intro to our tool: 
+
+Here is a quick intro to AalWines, using an interative 
+web-browser integration of our tool available at [demo.aalwines.cs.aau.dk](https://demo.aalwines.cs.aau.dk/):
 
 [![AalWiNes Quick Intro](http://img.youtube.com/vi/mvXAn9i7_Q0/0.jpg)](http://www.youtube.com/watch?v=mvXAn9i7_Q0 "AalWiNes Quick Intro")
 
 AalWiNes also allows to account for more complex traffic engineering aspects, such as load-balancing, 
-by supporting nondeterminism, as well as
-more complex multi-operation chains.
+by supporting nondeterminism, as well as more complex multi-operation chains.
 The tool includes several optimizations to further improve the performance, such as “top of stack reduction”,
 which safely calculates which labels can be at the top of stack in a given state of the PDA: the top of stack
 reduction technique greatly reduces the amount of transitions in the PDA.
 
 We refer to our [tool website](https://aalwines.cs.aau.dk/) as well as to our 
-[project website](https://github.com/DEIS-Tools/AalWiNes-Web).
+[project website](https://github.com/DEIS-Tools/AalWiNes).
 
 ## Conclusion and future work
 
@@ -128,3 +130,10 @@ Another interesting avenue for future research is
 the study of similar approaches for control plane verification
 or for supporting capacity planning, also taking into account
 resource constraints on failover paths. 
+
+## References
+
+\[1\] : P-Rex: Fast Verification of MPLS Networks with Multiple Link Failures. 
+Jesper Stenbjerg Jensen, Troels Beck Krogh, Jonas Sand Madsen, Stefan Schmid, Jiri Srba, 
+and Marc Tom Thorgersen. 14th ACM International Conference on emerging Networking EXperiments 
+and Technologies (CoNEXT), Heraklion/Crete, Greece, December 2018.