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

% 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{mathpazo} % Use the Palatino font by default

\usepackage{hyperref}

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

\usepackage{stmaryrd}

\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}

\usepackage{amsthm}

\usepackage{amssymb}

\usepackage{cleveref}

%\usepackage{mathtools}

\usepackage[noend]{algpseudocode}

\usepackage{enumitem}

\usepackage{nccmath}

\usepackage{tikz-cd}

\usepackage{tikz}

\usetikzlibrary{automata, positioning, calc}

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

%	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 work 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.

The reason behind this is that regex libraries in popular programming

languages often want to support richer constructs

than the usual basic regular expressions. Unfortunately, this means that even simple cases

are "infected" with atrocious running time.

This work aims to address the above vulnerability by a combination

of Brzozowski's derivatives and interactive theorem proving. We give an 

improved version of  Sulzmann and Lu's bit-coded algorithm using 

derivatives, and give a formal guarantee in terms of correctness and 

size of derivatives, which we formalised in Isabelle/HOL.

Then we improve the algorithm with a stronger version of 

simplification, and prove a time bound linear to input and

cubic to regular expression size using a technique introduced by

Antimirov.

The result is an algorithm with provable guarantees on 

work with these two guarantees together.

\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}

%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}