--- a/ChengsongTanPhdThesis/Chapters/RelatedWork.tex	Sat Oct 01 12:06:46 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/RelatedWork.tex	Mon Oct 03 02:08:49 2022 +0100
@@ -23,3 +23,29 @@
 flavours (e.g. whether references can be circular, 
 can labels be repeated etc.) of back-references syntax.
 
+
+\subsection{Matchers and Lexers with Mechanised Proofs}
+We are aware
+of a mechanised correctness proof of Brzozowski's derivative-based matcher in HOL4 by
+Owens and Slind~\parencite{Owens2008}. Another one in Isabelle/HOL is part
+of the work by Krauss and Nipkow \parencite{Krauss2011}.  And another one
+in Coq is given by Coquand and Siles \parencite{Coquand2012}.
+Also Ribeiro and Du Bois give one in Agda \parencite{RibeiroAgda2017}.
+ 
+\subsection{Static Analysis of Evil Regex Patterns} 
+ When a regular expression does not behave as intended,
+people usually try to rewrite the regex to some equivalent form
+or they try to avoid the possibly problematic patterns completely,
+for which many false positives exist\parencite{Davis18}.
+Animated tools to "debug" regular expressions such as
+ \parencite{regexploit2021} \parencite{regex101} are also popular.
+We are also aware of static analysis work on regular expressions that
+aims to detect potentially expoential regex patterns. Rathnayake and Thielecke 
+\parencite{Rathnayake2014StaticAF} proposed an algorithm
+that detects regular expressions triggering exponential
+behavious on backtracking matchers.
+Weideman \parencite{Weideman2017Static} came up with 
+non-linear polynomial worst-time estimates
+for regexes, attack string that exploit the worst-time 
+scenario, and "attack automata" that generates
+attack strings.