26 

    27 \subsection{Matchers and Lexers with Mechanised Proofs}

    28 We are aware

    29 of a mechanised correctness proof of Brzozowski's derivative-based matcher in HOL4 by

    30 Owens and Slind~\parencite{Owens2008}. Another one in Isabelle/HOL is part

    31 of the work by Krauss and Nipkow \parencite{Krauss2011}.  And another one

    32 in Coq is given by Coquand and Siles \parencite{Coquand2012}.

    33 Also Ribeiro and Du Bois give one in Agda \parencite{RibeiroAgda2017}.

    34  

    35 \subsection{Static Analysis of Evil Regex Patterns} 

    36  When a regular expression does not behave as intended,

    37 people usually try to rewrite the regex to some equivalent form

    38 or they try to avoid the possibly problematic patterns completely,

    39 for which many false positives exist\parencite{Davis18}.

    40 Animated tools to "debug" regular expressions such as

    41  \parencite{regexploit2021} \parencite{regex101} are also popular.

    42 We are also aware of static analysis work on regular expressions that

    43 aims to detect potentially expoential regex patterns. Rathnayake and Thielecke 

    44 \parencite{Rathnayake2014StaticAF} proposed an algorithm

    45 that detects regular expressions triggering exponential

    46 behavious on backtracking matchers.

    47 Weideman \parencite{Weideman2017Static} came up with 

    48 non-linear polynomial worst-time estimates

    49 for regexes, attack string that exploit the worst-time 

    50 scenario, and "attack automata" that generates

    51 attack strings.