|
1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
2 % Masters/Doctoral Thesis |
|
3 % LaTeX Template |
|
4 % Version 2.5 (27/8/17) |
|
5 % |
|
6 % This template was downloaded from: |
|
7 % http://www.LaTeXTemplates.com |
|
8 % |
|
9 % Version 2.x major modifications by: |
|
10 % Vel (vel@latextemplates.com) |
|
11 % |
|
12 % This template is based on a template by: |
|
13 % Steve Gunn (http://users.ecs.soton.ac.uk/srg/softwaretools/document/templates/) |
|
14 % Sunil Patel (http://www.sunilpatel.co.uk/thesis-template/) |
|
15 % |
|
16 % Template license: |
|
17 % CC BY-NC-SA 3.0 (http://creativecommons.org/licenses/by-nc-sa/3.0/) |
|
18 % |
|
19 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
20 |
|
21 %---------------------------------------------------------------------------------------- |
|
22 % PACKAGES AND OTHER DOCUMENT CONFIGURATIONS |
|
23 %---------------------------------------------------------------------------------------- |
|
24 |
|
25 \documentclass[ |
|
26 11pt, % The default document font size, options: 10pt, 11pt, 12pt |
|
27 %oneside, % Two side (alternating margins) for binding by default, uncomment to switch to one side |
|
28 english, % ngerman for German |
|
29 singlespacing, % Single line spacing, alternatives: onehalfspacing or doublespacing |
|
30 %draft, % Uncomment to enable draft mode (no pictures, no links, overfull hboxes indicated) |
|
31 %nolistspacing, % If the document is onehalfspacing or doublespacing, uncomment this to set spacing in lists to single |
|
32 %liststotoc, % Uncomment to add the list of figures/tables/etc to the table of contents |
|
33 %toctotoc, % Uncomment to add the main table of contents to the table of contents |
|
34 %parskip, % Uncomment to add space between paragraphs |
|
35 %nohyperref, % Uncomment to not load the hyperref package |
|
36 headsepline, % Uncomment to get a line under the header |
|
37 %chapterinoneline, % Uncomment to place the chapter title next to the number on one line |
|
38 %consistentlayout, % Uncomment to change the layout of the declaration, abstract and acknowledgements pages to match the default layout |
|
39 ]{MastersDoctoralThesis} % The class file specifying the document structure |
|
40 |
|
41 \usepackage[utf8]{inputenc} % Required for inputting international characters |
|
42 \usepackage[T1]{fontenc} % Output font encoding for international characters |
|
43 |
|
44 \usepackage{mathpazo} % Use the Palatino font by default |
|
45 \usepackage{hyperref} |
|
46 \usepackage[backend=bibtex,style=authoryear,natbib=true]{biblatex} % Use the bibtex backend with the authoryear citation style (which resembles APA) |
|
47 |
|
48 \addbibresource{example.bib} % The filename of the bibliography |
|
49 |
|
50 \usepackage[autostyle=true]{csquotes} % Required to generate language-dependent quotes in the bibliography |
|
51 |
|
52 %My Newly added Libraries in addition to template |
|
53 \usepackage{graphic} |
|
54 \usepackage{data} |
|
55 |
|
56 %\usepackage{algorithm} |
|
57 \usepackage{amsmath} |
|
58 \usepackage[noend]{algpseudocode} |
|
59 \usepackage{enumitem} |
|
60 \usepackage{nccmath} |
|
61 \usepackage{tikz-cd} |
|
62 \usetikzlibrary{positioning} |
|
63 |
|
64 %---------------------------------------------------------------------------------------- |
|
65 % MARGIN SETTINGS |
|
66 %---------------------------------------------------------------------------------------- |
|
67 |
|
68 \geometry{ |
|
69 paper=a4paper, % Change to letterpaper for US letter |
|
70 inner=2.5cm, % Inner margin |
|
71 outer=3.8cm, % Outer margin |
|
72 bindingoffset=.5cm, % Binding offset |
|
73 top=1.5cm, % Top margin |
|
74 bottom=1.5cm, % Bottom margin |
|
75 %showframe, % Uncomment to show how the type block is set on the page |
|
76 } |
|
77 |
|
78 %---------------------------------------------------------------------------------------- |
|
79 % THESIS INFORMATION |
|
80 %---------------------------------------------------------------------------------------- |
|
81 |
|
82 \thesistitle{POSIX Regular Expression Matching and Lexing} % Your thesis title, this is used in the title and abstract, print it elsewhere with \ttitle |
|
83 \supervisor{Dr. Christian \textsc{Urban}} % Your supervisor's name, this is used in the title page, print it elsewhere with \supname |
|
84 \examiner{} % Your examiner's name, this is not currently used anywhere in the template, print it elsewhere with \examname |
|
85 \degree{Doctor of Philosophy} % Your degree name, this is used in the title page and abstract, print it elsewhere with \degreename |
|
86 \author{Chengsong \textsc{Tan}} % Your name, this is used in the title page and abstract, print it elsewhere with \authorname |
|
87 \addresses{} % Your address, this is not currently used anywhere in the template, print it elsewhere with \addressname |
|
88 |
|
89 \subject{Computer Science} % Your subject area, this is not currently used anywhere in the template, print it elsewhere with \subjectname |
|
90 \keywords{} % Keywords for your thesis, this is not currently used anywhere in the template, print it elsewhere with \keywordnames |
|
91 \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 |
|
92 \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 |
|
93 \group{\href{https://www.kcl.ac.uk/research/ssy}{Software Systems}} % Your research group's name and URL, this is used in the title page, print it elsewhere with \groupname |
|
94 \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 |
|
95 |
|
96 \AtBeginDocument{ |
|
97 \hypersetup{pdftitle=\ttitle} % Set the PDF's title to your title |
|
98 \hypersetup{pdfauthor=\authorname} % Set the PDF's author to your name |
|
99 \hypersetup{pdfkeywords=\keywordnames} % Set the PDF's keywords to your keywords |
|
100 } |
|
101 |
|
102 \begin{document} |
|
103 |
|
104 \frontmatter % Use roman page numbering style (i, ii, iii, iv...) for the pre-content pages |
|
105 |
|
106 \pagestyle{plain} % Default to the plain heading style until the thesis style is called for the body content |
|
107 |
|
108 %---------------------------------------------------------------------------------------- |
|
109 % TITLE PAGE |
|
110 %---------------------------------------------------------------------------------------- |
|
111 |
|
112 \begin{titlepage} |
|
113 \begin{center} |
|
114 |
|
115 \vspace*{.06\textheight} |
|
116 {\scshape\LARGE \univname\par}\vspace{1.5cm} % University name |
|
117 \textsc{\Large Doctoral Thesis}\\[0.5cm] % Thesis type |
|
118 |
|
119 \HRule \\[0.4cm] % Horizontal line |
|
120 {\huge \bfseries \ttitle\par}\vspace{0.4cm} % Thesis title |
|
121 \HRule \\[1.5cm] % Horizontal line |
|
122 |
|
123 \begin{minipage}[t]{0.4\textwidth} |
|
124 \begin{flushleft} \large |
|
125 \emph{Author:}\\ |
|
126 \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 |
|
127 \end{flushleft} |
|
128 \end{minipage} |
|
129 |
|
130 |
|
131 \begin{minipage}[t]{0.4\textwidth} |
|
132 \begin{flushright} \large |
|
133 \emph{Supervisor:} \\ |
|
134 \href{https://www.kcl.ac.uk/people/christian-urban}{\supname} % Supervisor name - remove the \href bracket to remove the link |
|
135 \end{flushright} |
|
136 \end{minipage}\\[3cm] |
|
137 |
|
138 \vfill |
|
139 |
|
140 \large \textit{A thesis submitted in fulfillment of the requirements\\ for the degree of \degreename}\\[0.3cm] % University requirement text |
|
141 \textit{in the}\\[0.4cm] |
|
142 \groupname\\\deptname\\[2cm] % Research group name and department name |
|
143 |
|
144 \vfill |
|
145 |
|
146 {\large \today}\\[4cm] % Date |
|
147 %\includegraphics{Logo} % University/department logo - uncomment to place it |
|
148 |
|
149 \vfill |
|
150 \end{center} |
|
151 \end{titlepage} |
|
152 |
|
153 %---------------------------------------------------------------------------------------- |
|
154 % DECLARATION PAGE |
|
155 %---------------------------------------------------------------------------------------- |
|
156 |
|
157 \begin{declaration} |
|
158 \addchaptertocentry{\authorshipname} % Add the declaration to the table of contents |
|
159 \noindent I, \authorname, declare that this thesis titled, \enquote{\ttitle} and the work presented in it are my own. I confirm that: |
|
160 |
|
161 \begin{itemize} |
|
162 \item This work was done wholly or mainly while in candidature for a research degree at this University. |
|
163 \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. |
|
164 \item Where I have consulted the published work of others, this is always clearly attributed. |
|
165 \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. |
|
166 \item I have acknowledged all main sources of help. |
|
167 \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.\\ |
|
168 \end{itemize} |
|
169 |
|
170 \noindent Signed:\\ |
|
171 \rule[0.5em]{25em}{0.5pt} % This prints a line for the signature |
|
172 |
|
173 \noindent Date:\\ |
|
174 \rule[0.5em]{25em}{0.5pt} % This prints a line to write the date |
|
175 \end{declaration} |
|
176 |
|
177 \cleardoublepage |
|
178 |
|
179 %---------------------------------------------------------------------------------------- |
|
180 % QUOTATION PAGE |
|
181 %---------------------------------------------------------------------------------------- |
|
182 |
|
183 \vspace*{0.2\textheight} |
|
184 |
|
185 \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 |
|
186 |
|
187 \hfill Dave Barry |
|
188 |
|
189 %---------------------------------------------------------------------------------------- |
|
190 % ABSTRACT PAGE |
|
191 %---------------------------------------------------------------------------------------- |
|
192 |
|
193 \begin{abstract} |
|
194 \addchaptertocentry{\abstractname} % Add the abstract to the table of contents |
|
195 This work is a combination of functional algorithms |
|
196 and formal methods. |
|
197 Regular expression matching and lexing has been |
|
198 widely-used and well-implemented |
|
199 in software industry. |
|
200 |
|
201 Theoretical results say that regular expression matching |
|
202 should be linear with respect to the input. |
|
203 Under a certain class of regular expressions and inputs though, |
|
204 practical implementations suffer from non-linear or even |
|
205 exponential running time, |
|
206 allowing a ReDoS (regular expression denial-of-service ) attack. |
|
207 |
|
208 |
|
209 The reason behind is that regex libraries in popular language engines |
|
210 often want to support richer constructs |
|
211 than the most basic regular expressions, and lexing rather than matching |
|
212 is needed for sub-match extraction. |
|
213 |
|
214 This work aims to address the above vulnerability by the combination |
|
215 of Brzozowski's derivatives and interactive theorem proving. We give an |
|
216 improved version of Sulzmann and Lu's bit-coded algorithm using |
|
217 derivatives, which come with a formal guarantee in terms of correctness and |
|
218 running time as an Isabelle/HOL proof. |
|
219 Then we improve the algorithm with an even stronger version of |
|
220 simplification, and prove a time bound linear to input and |
|
221 cubic to regular expression size using a technique by |
|
222 Antimirov. |
|
223 |
|
224 |
|
225 |
|
226 |
|
227 \end{abstract} |
|
228 |
|
229 %---------------------------------------------------------------------------------------- |
|
230 % ACKNOWLEDGEMENTS |
|
231 %---------------------------------------------------------------------------------------- |
|
232 |
|
233 \begin{acknowledgements} |
|
234 \addchaptertocentry{\acknowledgementname} % Add the acknowledgements to the table of contents |
|
235 The acknowledgments and the people to thank go here, don't forget to include your project advisor\ldots |
|
236 \end{acknowledgements} |
|
237 |
|
238 %---------------------------------------------------------------------------------------- |
|
239 % LIST OF CONTENTS/FIGURES/TABLES PAGES |
|
240 %---------------------------------------------------------------------------------------- |
|
241 |
|
242 \tableofcontents % Prints the main table of contents |
|
243 |
|
244 \listoffigures % Prints the list of figures |
|
245 |
|
246 \listoftables % Prints the list of tables |
|
247 |
|
248 %---------------------------------------------------------------------------------------- |
|
249 % ABBREVIATIONS |
|
250 %---------------------------------------------------------------------------------------- |
|
251 |
|
252 \begin{abbreviations}{ll} % Include a list of abbreviations (a table of two columns) |
|
253 |
|
254 \textbf{LAH} & \textbf{L}ist \textbf{A}bbreviations \textbf{H}ere\\ |
|
255 \textbf{WSF} & \textbf{W}hat (it) \textbf{S}tands \textbf{F}or\\ |
|
256 |
|
257 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% |
|
258 \newcommand{\ZERO}{\mbox{\bf 0}} |
|
259 \newcommand{\ONE}{\mbox{\bf 1}} |
|
260 \def\lexer{\mathit{lexer}} |
|
261 \def\mkeps{\mathit{mkeps}} |
|
262 |
|
263 \def\DFA{\textit{DFA}} |
|
264 \def\bmkeps{\textit{bmkeps}} |
|
265 \def\retrieve{\textit{retrieve}} |
|
266 \def\blexer{\textit{blexer}} |
|
267 \def\flex{\textit{flex}} |
|
268 \def\inj{\mathit{inj}} |
|
269 \def\Empty{\mathit{Empty}} |
|
270 \def\Left{\mathit{Left}} |
|
271 \def\Right{\mathit{Right}} |
|
272 \def\Stars{\mathit{Stars}} |
|
273 \def\Char{\mathit{Char}} |
|
274 \def\Seq{\mathit{Seq}} |
|
275 \def\Der{\mathit{Der}} |
|
276 \def\nullable{\mathit{nullable}} |
|
277 \def\Z{\mathit{Z}} |
|
278 \def\S{\mathit{S}} |
|
279 \def\rup{r^\uparrow} |
|
280 |
|
281 \end{abbreviations} |
|
282 |
|
283 %---------------------------------------------------------------------------------------- |
|
284 % PHYSICAL CONSTANTS/OTHER DEFINITIONS |
|
285 %---------------------------------------------------------------------------------------- |
|
286 |
|
287 \begin{constants}{lr@{${}={}$}l} % The list of physical constants is a three column table |
|
288 |
|
289 % The \SI{}{} command is provided by the siunitx package, see its documentation for instructions on how to use it |
|
290 |
|
291 Speed of Light & $c_{0}$ & \SI{2.99792458e8}{\meter\per\second} (exact)\\ |
|
292 %Constant Name & $Symbol$ & $Constant Value$ with units\\ |
|
293 |
|
294 \end{constants} |
|
295 |
|
296 %---------------------------------------------------------------------------------------- |
|
297 % SYMBOLS |
|
298 %---------------------------------------------------------------------------------------- |
|
299 |
|
300 \begin{symbols}{lll} % Include a list of Symbols (a three column table) |
|
301 |
|
302 $a$ & distance & \si{\meter} \\ |
|
303 $P$ & power & \si{\watt} (\si{\joule\per\second}) \\ |
|
304 %Symbol & Name & Unit \\ |
|
305 |
|
306 \addlinespace % Gap to separate the Roman symbols from the Greek |
|
307 |
|
308 $\omega$ & angular frequency & \si{\radian} \\ |
|
309 |
|
310 \end{symbols} |
|
311 |
|
312 %---------------------------------------------------------------------------------------- |
|
313 % DEDICATION |
|
314 %---------------------------------------------------------------------------------------- |
|
315 |
|
316 \dedicatory{For/Dedicated to/To my\ldots} |
|
317 |
|
318 %---------------------------------------------------------------------------------------- |
|
319 % THESIS CONTENT - CHAPTERS |
|
320 %---------------------------------------------------------------------------------------- |
|
321 |
|
322 \mainmatter % Begin numeric (1,2,3...) page numbering |
|
323 |
|
324 \pagestyle{thesis} % Return the page headers back to the "thesis" style |
|
325 |
|
326 % Include the chapters of the thesis as separate files from the Chapters folder |
|
327 % Uncomment the lines as you write the chapters |
|
328 |
|
329 \include{Chapters/Chapter1} |
|
330 \include{Chapters/Chapter2} |
|
331 \include{Chapters/Chapter3} |
|
332 %\include{Chapters/Chapter4} |
|
333 %\include{Chapters/Chapter5} |
|
334 |
|
335 %---------------------------------------------------------------------------------------- |
|
336 % THESIS CONTENT - APPENDICES |
|
337 %---------------------------------------------------------------------------------------- |
|
338 |
|
339 \appendix % Cue to tell LaTeX that the following "chapters" are Appendices |
|
340 |
|
341 % Include the appendices of the thesis as separate files from the Appendices folder |
|
342 % Uncomment the lines as you write the Appendices |
|
343 |
|
344 \include{Appendices/AppendixA} |
|
345 %\include{Appendices/AppendixB} |
|
346 %\include{Appendices/AppendixC} |
|
347 |
|
348 %---------------------------------------------------------------------------------------- |
|
349 % BIBLIOGRAPHY |
|
350 %---------------------------------------------------------------------------------------- |
|
351 |
|
352 \printbibliography[heading=bibintoc] |
|
353 |
|
354 %---------------------------------------------------------------------------------------- |
|
355 |
|
356 \end{document} |