33 %toctotoc, % Uncomment to add the main table of contents 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 |
34 %parskip, % Uncomment to add space between paragraphs |
35 %nohyperref, % Uncomment to not load the hyperref package |
35 %nohyperref, % Uncomment to not load the hyperref package |
36 headsepline, % Uncomment to get a line under the header |
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 |
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 |
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 |
39 ]{MastersDoctoralThesis} % The class file specifying the document structure |
40 |
40 |
41 \usepackage[utf8]{inputenc} % Required for inputting international characters |
41 \usepackage[utf8]{inputenc} % Required for inputting international characters |
42 \usepackage[T1]{fontenc} % Output font encoding for international characters |
42 \usepackage[T1]{fontenc} % Output font encoding for international characters |
43 |
43 |
89 |
89 |
90 \subject{Computer Science} % Your subject area, this is not currently used anywhere in the template, print it elsewhere with \subjectname |
90 \subject{Computer Science} % Your subject area, this is not currently used anywhere in the template, print it elsewhere with \subjectname |
91 \keywords{} % Keywords for your thesis, this is not currently used anywhere in the template, print it elsewhere with \keywordnames |
91 \keywords{} % Keywords for your thesis, this is not currently used anywhere in the template, print it elsewhere with \keywordnames |
92 \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 \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 |
93 \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 \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 |
94 \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 \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 |
95 \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 \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 |
96 |
96 |
97 \AtBeginDocument{ |
97 \AtBeginDocument{ |
98 \hypersetup{pdftitle=\ttitle} % Set the PDF's title to your title |
98 \hypersetup{pdftitle=\ttitle} % Set the PDF's title to your title |
99 \hypersetup{pdfauthor=\authorname} % Set the PDF's author to your name |
99 \hypersetup{pdfauthor=\authorname} % Set the PDF's author to your name |
191 % ABSTRACT PAGE |
191 % ABSTRACT PAGE |
192 %---------------------------------------------------------------------------------------- |
192 %---------------------------------------------------------------------------------------- |
193 |
193 |
194 \begin{abstract} |
194 \begin{abstract} |
195 \addchaptertocentry{\abstractname} % Add the abstract to the table of contents |
195 \addchaptertocentry{\abstractname} % Add the abstract to the table of contents |
196 This work is a combination of functional algorithms |
196 This work is about regular expressions and derivatives. It combines functional algorithms and their formal verification in the Isabelle/HOL theorem prover. |
197 and formal methods. |
|
198 Regular expression matching and lexing has been |
|
199 widely-used and well-implemented |
|
200 in software industry. |
|
201 |
197 |
202 Theoretical results say that regular expression matching |
198 Theoretical results say that regular expression matching |
203 should be linear with respect to the input. |
199 should be linear with respect to the input. |
204 Under a certain class of regular expressions and inputs though, |
200 Under a certain class of regular expressions and inputs though, |
205 practical implementations suffer from non-linear or even |
201 practical implementations suffer from non-linear or even |