lexing: comparison ChengsongTanPhdThesis/Chapters/Introduction.tex

equal deleted inserted replaced

-:d50a309a0645
+:bdb3ffdd39f8
 maintained.
 \end{itemize}
 \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.
 simplifications fail to simplify. We therefore introduce our version of the
 algorithm with simplification and
 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.
+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
+improve the finite bound to a cubic bound.%and the NOT regular expression.
-algorithm to include bounded repetitions. %and the NOT regular expression.