--- a/ChengsongTanPhdThesis/Chapters/RelatedWork.tex Tue Jul 25 17:28:29 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/RelatedWork.tex Wed Aug 23 03:02:31 2023 +0100
@@ -291,6 +291,14 @@
%flavours of back-references syntax (e.g. whether references can be circular,
%can labels be repeated etc.).
+The recently published work on formally verified lexer
+\cite{Margus2023PLDI} by Moseley et al.
+moves a big step forward in practical performance--their lexer can compete
+with unverified commercial regex engines like those in Java, Python and etc.
+and supports lookaheads.
+To reach their speed on larger datasets like \cite{TwainRegex}, one has to
+incorporate many fine-tunings and one of the first modifications needed would
+be to drop whole-string lexing but only extract the submatch needed by the user.