%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Masters/Doctoral Thesis 

% LaTeX Template

% Version 2.5 (27/8/17)

%

% This template was downloaded from:

% http://www.LaTeXTemplates.com

%

% Version 2.x major modifications by:

% Vel (vel@latextemplates.com)

%

% This template is based on a template by:

% Steve Gunn (http://users.ecs.soton.ac.uk/srg/softwaretools/document/templates/)

% Sunil Patel (http://www.sunilpatel.co.uk/thesis-template/)

%

% Template license:

% CC BY-NC-SA 3.0 (http://creativecommons.org/licenses/by-nc-sa/3.0/)

%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%----------------------------------------------------------------------------------------

%	PACKAGES AND OTHER DOCUMENT CONFIGURATIONS

%----------------------------------------------------------------------------------------

\documentclass[

11pt, % The default document font size, options: 10pt, 11pt, 12pt

%oneside, % Two side (alternating margins) for binding by default, uncomment to switch to one side

english, % ngerman for German

singlespacing, % Single line spacing, alternatives: onehalfspacing or doublespacing

%draft, % Uncomment to enable draft mode (no pictures, no links, overfull hboxes indicated)

%nolistspacing, % If the document is onehalfspacing or doublespacing, uncomment this to set spacing in lists to single

%liststotoc, % Uncomment to add the list of figures/tables/etc to the table of contents

%toctotoc, % Uncomment to add the main table of contents to the table of contents

%parskip, % Uncomment to add space between paragraphs

%nohyperref, % Uncomment to not load the hyperref package

headsepline, % Uncomment to get a line under the header

%chapterinoneline, % Uncomment to place the chapter title next to the number on one line

consistentlayout, % Uncomment to change the layout of the declaration, abstract and acknowledgements pages to match the default layout

]{MastersDoctoralThesis} % The class file specifying the document structure

\usepackage[utf8]{inputenc} % Required for inputting international characters

\usepackage[T1]{fontenc} % Output font encoding for international characters

%\usepackage{fdsymbol} % Loads unicode-math

\usepackage{cancel}

\usepackage{verbatim}

\usepackage{float}

\usepackage{mathpazo} % Use the Palatino font by default

\usepackage{hyperref}

\usepackage{lipsum}

\usepackage[backend=bibtex]{biblatex} % Use the bibtex backend with the authoryear citation style (which resembles APA)

\usepackage[usestackEOL]{stackengine}

\usepackage{scalerel}

\usepackage{graphicx}

%style=authoryear, natbib=true 

\usepackage{stmaryrd}

\usepackage{caption}

\addbibresource{example.bib} % The filename of the bibliography

\usepackage[autostyle=true]{csquotes} % Required to generate language-dependent quotes in the bibliography

%My Newly added Libraries in addition to template

\usepackage{graphic}

\usepackage{data}

%\usepackage{algorithm}

\usepackage{amsmath}

\makeatletter

\newcommand{\xleftrightarrow}[2][]{\ext@arrow 3359\leftrightarrowfill@{#1}{#2}}

\newcommand{\xdashrightarrow}[2][]{\ext@arrow 0359\rightarrowfill@@{#1}{#2}}

\newcommand{\xdashleftarrow}[2][]{\ext@arrow 3095\leftarrowfill@@{#1}{#2}}

\newcommand{\xdashleftrightarrow}[2][]{\ext@arrow 3359\leftrightarrowfill@@{#1}{#2}}

\def\rightarrowfill@@{\arrowfill@@\relax\relbar\rightarrow}

\def\leftarrowfill@@{\arrowfill@@\leftarrow\relbar\relax}

\def\leftrightarrowfill@@{\arrowfill@@\leftarrow\relbar\rightarrow}

\def\arrowfill@@#1#2#3#4{%

  $\m@th\thickmuskip0mu\medmuskip\thickmuskip\thinmuskip\thickmuskip

   \relax#4#1

   \xleaders\hbox{$#4#2$}\hfill

   #3$%

}

\makeatother

\def\checkmark{\tikz\fill[scale=0.4](0,.35) -- (.25,0) -- (1,.7) -- (.25,.15) -- cycle;} 

\usepackage{amsthm}

\usepackage{amssymb}

\usepackage{cleveref}

%\usepackage{mathtools}

\usepackage[noend]{algpseudocode}

\usepackage{enumitem}

\usepackage{nccmath}

\usepackage{tikz-cd}

\usepackage{tikz}

\usetikzlibrary{automata, positioning, calc}

\usetikzlibrary{arrows}

\usetikzlibrary{shapes.misc}

\usetikzlibrary{fit,

                shapes.geometric,

		patterns,

		backgrounds,

		graphs}

\usetikzlibrary{babel}

\usepackage{mathpartir}

\usepackage{stackrel}

\DeclareCaptionType{mytype}[Illustration][]

\newenvironment{envForCaption}{\captionsetup{type=mytype} }{}

%----------------------------------------------------------------------------------------

%	MARGIN SETTINGS

%----------------------------------------------------------------------------------------

\geometry{

	paper=a4paper, % Change to letterpaper for US letter

	inner=2.5cm, % Inner margin

	outer=3.8cm, % Outer margin

	bindingoffset=.5cm, % Binding offset

	top=1.5cm, % Top margin

	bottom=1.5cm, % Bottom margin

	%showframe, % Uncomment to show how the type block is set on the page

}

%----------------------------------------------------------------------------------------

%	THESIS INFORMATION

%----------------------------------------------------------------------------------------

\thesistitle{POSIX Regular Expression Matching and Lexing} % Your thesis title, this is used in the title and abstract, print it elsewhere with \ttitle

\supervisor{Dr. Christian \textsc{Urban}} % Your supervisor's name, this is used in the title page, print it elsewhere with \supname

\examiner{} % Your examiner's name, this is not currently used anywhere in the template, print it elsewhere with \examname

\degree{Doctor of Philosophy} % Your degree name, this is used in the title page and abstract, print it elsewhere with \degreename

\author{Chengsong \textsc{Tan}} % Your name, this is used in the title page and abstract, print it elsewhere with \authorname

\addresses{} % Your address, this is not currently used anywhere in the template, print it elsewhere with \addressname

\subject{Computer Science} % Your subject area, this is not currently used anywhere in the template, print it elsewhere with \subjectname

\keywords{} % Keywords for your thesis, this is not currently used anywhere in the template, print it elsewhere with \keywordnames

\university{\href{https://www.kcl.ac.uk}{King's College London}} % Your university's name and URL, this is used in the title page and abstract, print it elsewhere with \univname

\department{\href{https://www.kcl.ac.uk/informatics}{Department or Informatics}} % Your department's name and URL, this is used in the title page and abstract, print it elsewhere with \deptname

\group{\href{https://www.kcl.ac.uk/research/ssy}{Software Systems Group}} % Your research group's name and URL, this is used in the title page, print it elsewhere with \groupname

\faculty{\href{http://faculty.university.com}{Chengsong Tan}} % Your faculty's name and URL, this is used in the title page and abstract, print it elsewhere with \facname

\AtBeginDocument{

\hypersetup{pdftitle=\ttitle} % Set the PDF's title to your title

\hypersetup{pdfauthor=\authorname} % Set the PDF's author to your name

\hypersetup{pdfkeywords=\keywordnames} % Set the PDF's keywords to your keywords

}

\begin{document}

\frontmatter % Use roman page numbering style (i, ii, iii, iv...) for the pre-content pages

\pagestyle{plain} % Default to the plain heading style until the thesis style is called for the body content

%----------------------------------------------------------------------------------------

%	TITLE PAGE

%----------------------------------------------------------------------------------------

\begin{titlepage}

\begin{center}

\vspace*{.06\textheight}

{\scshape\LARGE \univname\par}\vspace{1.5cm} % University name

\textsc{\Large Doctoral Thesis}\\[0.5cm] % Thesis type

\HRule \\[0.4cm] % Horizontal line

{\huge \bfseries \ttitle\par}\vspace{0.4cm} % Thesis title

\HRule \\[1.5cm] % Horizontal line

\begin{minipage}[t]{0.4\textwidth}

\begin{flushleft} \large

\emph{Author:}\\

\href{https://kclpure.kcl.ac.uk/portal/en/persons/chengsong-tan(a63b381b-04bc-4cd7-beea-beb3e96cb153).html}{\authorname} % Author name - remove the \href bracket to remove the link

\end{flushleft}

\end{minipage}

\begin{minipage}[t]{0.4\textwidth}

\begin{flushright} \large

\emph{Supervisor:} \\

\href{https://www.kcl.ac.uk/people/christian-urban}{\supname} % Supervisor name - remove the \href bracket to remove the link  

\end{flushright}

\end{minipage}\\[3cm]

\vfill

\large \textit{A thesis submitted in fulfillment of the requirements\\ for the degree of \degreename}\\[0.3cm] % University requirement text

\textit{in the}\\[0.4cm]

\groupname\\\deptname\\[2cm] % Research group name and department name

\vfill

{\large \today}\\[4cm] % Date

%\includegraphics{Logo} % University/department logo - uncomment to place it

\vfill

\end{center}

\end{titlepage}

%----------------------------------------------------------------------------------------

%	DECLARATION PAGE

%----------------------------------------------------------------------------------------

\begin{declaration}

\addchaptertocentry{\authorshipname} % Add the declaration to the table of contents

\noindent I, \authorname, declare that this thesis titled, \enquote{\ttitle} and the work presented in it are my own. I confirm that:

\begin{itemize} 

\item This work was done wholly or mainly while in candidature for a research degree at this University.

\item Where any part of this thesis has previously been submitted for a degree or any other qualification at this University or any other institution, this has been clearly stated.

\item Where I have consulted the published work of others, this is always clearly attributed.

\item Where I have quoted from the work of others, the source is always given. With the exception of such quotations, this thesis is entirely my own work.

\item I have acknowledged all main sources of help.

\item Where the thesis is based on work done by myself jointly with others, I have made clear exactly what was done by others and what I have contributed myself.\\

\end{itemize}

\noindent Signed:\\

\rule[0.5em]{25em}{0.5pt} % This prints a line for the signature

\noindent Date:\\

\rule[0.5em]{25em}{0.5pt} % This prints a line to write the date

\end{declaration}

\cleardoublepage

%----------------------------------------------------------------------------------------

%	QUOTATION PAGE

%----------------------------------------------------------------------------------------

\vspace*{0.2\textheight}

\noindent\enquote{\itshape Thanks to my solid academic training, today I can write hundreds of words on virtually any topic without possessing a shred of information, which is how I got a good job in journalism.}\bigbreak

\hfill Dave Barry

%----------------------------------------------------------------------------------------

%	ABSTRACT PAGE

%----------------------------------------------------------------------------------------

%\begin{abstract}

%\end{abstract}

\begin{abstract}

\addchaptertocentry{\abstractname} % Add the abstract to the table of contents

%\addchap{Abstract} 

This thesis is about regular expressions and derivatives. It combines functional algorithms and their formal verification in the Isabelle/HOL theorem prover. 

Theoretical results say that regular expression matching should be linear with respect to the input. Under a certain class of regular expressions and inputs though, practical implementations often suffer from non-linear or even exponential running time, allowing ReDoS (regular expression denial-of-service ) attacks. This makes levers with formalised properties such as correctness and time complexity appealing.

Sulzmann and Lu describe a lexing algorithm that calculates Brzozowski derivatives using bitcodes annotated to regular expressions. Their algorithm generates POSIX values which encode the information of how a regular expression matches a string—that is, which part of the string is matched by which part of the regular expression. This information is needed in the context of lexing in order to extract and to classify tokens. The purpose of the bitcodes is to generate POSIX values incrementally while derivatives are calculated. They also help with designing an “aggressive” simplification function that keeps the size of derivatives finitely bounded. Without simplification the size of some derivatives can grow arbitrarily big resulting in an extremely slow lexing algorithm. 

In this thesis we describe a variant of Sulzmann and Lu’s algorithm: Our variant is a recursive functional program, whereas Sulzmann and Lu’s version involves a fixpoint construction. We (i) prove in Isabelle/HOL that our algorithm is correct and generates unique POSIX values; we also (ii) establish a finite bound for the size of the derivatives. 

\end{abstract}

%----------------------------------------------------------------------------------------

%	ACKNOWLEDGEMENTS

%----------------------------------------------------------------------------------------

\begin{acknowledgements}

\addchaptertocentry{\acknowledgementname} % Add the acknowledgements to the table of contents

The acknowledgments and the people to thank go here, don't forget to include your project advisor\ldots

\end{acknowledgements}

%----------------------------------------------------------------------------------------

%	LIST OF CONTENTS/FIGURES/TABLES PAGES

%----------------------------------------------------------------------------------------

\tableofcontents % Prints the main table of contents

%\listoffigures % Prints the list of figures

%\listoftables % Prints the list of tables

%----------------------------------------------------------------------------------------

%	ABBREVIATIONS

%----------------------------------------------------------------------------------------

\begin{abbreviations}{ll} % Include a list of abbreviations (a table of two columns)

\newtheorem{theorem}{Theorem}

\newtheorem{lemma}{Lemma}

\newtheorem{definition}{Definition}

\newtheorem{conjecture}{Conjecture}

\newtheorem{corollary}{Corollary}

\newtheorem{property}{Property}

\newtheorem{proposition}{Proposition}

%proof

\newcommand\sflat[1][]{\textit{sflat} \, #1}

\newcommand{\ASEQ}[3]{\textit{ASEQ}_{#1} \, #2 \, #3}

\newcommand{\bderssimp}[2]{#1 \backslash_{bsimp} #2}

\newcommand{\rderssimp}[2]{#1 \backslash_{rsimp} #2}

\newcommand{\sflataux}[1]{\lbracket #1 \rbracket}

\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%

\newcommand{\ZERO}{\mbox{\bf 0}}

\newcommand{\ONE}{\mbox{\bf 1}}

\newcommand{\AALTS}[2]{\XOR {\scriptstyle #1}\, #2}

\def\lexer{\mathit{lexer}}

\def\mkeps{\mathit{mkeps}}

\def\AZERO{\textit{AZERO}}

\def\AONE{\textit{AONE}}

\def\ACHAR{\textit{ACHAR}}

\def\ALTS{\textit{ALTS}}

\def\ASTAR{\textit{ASTAR}}

\def\DFA{\textit{DFA}}

\def\bmkeps{\textit{bmkeps}}

\def\retrieve{\textit{retrieve}}

\def\blexer{\textit{blexer}}

\def\flex{\textit{flex}}

\def\inj{\mathit{inj}}

\def\Empty{\mathit{Empty}}

\def\Left{\mathit{Left}}

\def\Right{\mathit{Right}}

\def\Stars{\mathit{Stars}}

\def\Char{\mathit{Char}}

\def\Seq{\mathit{Seq}}

\def\Der{\mathit{Der}}

\def\nullable{\mathit{nullable}}

\def\Z{\mathit{Z}}

\def\S{\mathit{S}}

\def\rup{r^\uparrow}

%\def\bderssimp{\mathit{bders}\_\mathit{simp}}

\def\distinctWith{\textit{distinctWith}}

\def\rexp{\mathbf{rexp}}

\def\simp{\mathit{simp}}

\def\simpALTs{\mathit{simp}\_\mathit{ALTs}}

\def\map{\mathit{map}}

\def\distinct{\mathit{distinct}}

\def\blexersimp{\mathit{blexer}\_\mathit{simp}}

\def\map{\textit{map}}

\def\vsuf{\textit{vsuf}}

\def\sflataux{\textit{sflat}\_\textit{aux}}

\def\rrexp{\textit{rrexp}}

\def\rsize{\textit{rsize}}

\def\asize{\textit{asize}}

\def\rerase{\textit{rerase}}

\def\erase{\textit{erase}}

\def\STAR{\textit{STAR}}

\def\flts{\textit{flts}}

\end{abbreviations}

%----------------------------------------------------------------------------------------

%	SYMBOLS

%----------------------------------------------------------------------------------------

%\begin{symbols}{lll} % Include a list of Symbols (a three column table)

%$a$ & distance & \si{\meter} \\

%$P$ & power & \si{\watt} (\si{\joule\per\second}) \\

%Symbol & Name & Unit \\

%\addlinespace % Gap to separate the Roman symbols from the Greek

%$\omega$ & angular frequency & \si{\radian} \\

%\end{symbols}

%----------------------------------------------------------------------------------------

%	DEDICATION

%----------------------------------------------------------------------------------------

\dedicatory{For/Dedicated to/To my\ldots} 

%----------------------------------------------------------------------------------------

%	THESIS CONTENT - CHAPTERS

%----------------------------------------------------------------------------------------

\mainmatter % Begin numeric (1,2,3...) page numbering

\pagestyle{thesis} % Return the page headers back to the "thesis" style

% Include the chapters of the thesis as separate files from the Chapters folder

% Uncomment the lines as you write the chapters

\include{Chapters/Introduction}

\include{Chapters/Inj} 

\include{Chapters/Bitcoded1}

\include{Chapters/Bitcoded2}

\include{Chapters/Finite} 

\include{Chapters/Cubic}

\include{Chapters/Further}

%----------------------------------------------------------------------------------------

%	THESIS CONTENT - APPENDICES

%----------------------------------------------------------------------------------------

\appendix % Cue to tell LaTeX that the following "chapters" are Appendices

% Include the appendices of the thesis as separate files from the Appendices folder

% Uncomment the lines as you write the Appendices

\include{Appendices/AppendixA}

%\include{Appendices/AppendixB}

%\include{Appendices/AppendixC}

%----------------------------------------------------------------------------------------

%	BIBLIOGRAPHY

%----------------------------------------------------------------------------------------

\printbibliography[heading=bibintoc]

%----------------------------------------------------------------------------------------

\end{document}