--- a/ChengsongTanPhdThesis/Chapters/Introduction.tex	Mon Dec 05 17:39:10 2022 +0000
+++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex	Thu Dec 08 00:19:56 2022 +0000
@@ -1245,8 +1245,15 @@
 \noindent
 With a formal finiteness bound in place,
 we can greatly reduce the attack surface of servers in terms of ReDoS attacks.
+The Isabelle/HOL code for our formalisation can be 
+found at
+\begin{center}
+\url{https://github.com/hellotommmy/posix}
+\end{center}
 Further improvements to the algorithm with an even stronger version of 
-simplification can be made.
+simplification can be made. We conjecture that the resulting size of derivatives
+can be bounded by a cubic bound w.r.t. the size of the regular expression.
+
 
 
 
@@ -1267,10 +1274,11 @@
 its correctness proof .  
 In chapter \ref{Finite} we give the second guarantee
 of our bitcoded algorithm, that is a finite bound on the size of any 
-regular expression's derivatives.
+regular expression's derivatives. 
+We also show how one can extend the
+algorithm to include bounded repetitions. 
 In chapter \ref{Cubic} we discuss stronger simplification rules which 
-improve the finite bound to a polynomial bound, and also show how one can extend the
-algorithm to include bounded repetitions. %and the NOT regular expression.
+improve the finite bound to a cubic bound.%and the NOT regular expression.