equal
deleted
inserted
replaced
57 |
57 |
58 %\usepackage{algorithm} |
58 %\usepackage{algorithm} |
59 \usepackage{amsmath} |
59 \usepackage{amsmath} |
60 \usepackage{amsthm} |
60 \usepackage{amsthm} |
61 \usepackage{amssymb} |
61 \usepackage{amssymb} |
|
62 \usepackage{cleveref} |
62 %\usepackage{mathtools} |
63 %\usepackage{mathtools} |
63 \usepackage[noend]{algpseudocode} |
64 \usepackage[noend]{algpseudocode} |
64 \usepackage{enumitem} |
65 \usepackage{enumitem} |
65 \usepackage{nccmath} |
66 \usepackage{nccmath} |
66 \usepackage{tikz-cd} |
67 \usepackage{tikz-cd} |
194 |
195 |
195 %---------------------------------------------------------------------------------------- |
196 %---------------------------------------------------------------------------------------- |
196 % ABSTRACT PAGE |
197 % ABSTRACT PAGE |
197 %---------------------------------------------------------------------------------------- |
198 %---------------------------------------------------------------------------------------- |
198 |
199 |
199 \begin{abstract} |
200 %\begin{abstract} |
|
201 |
|
202 |
|
203 %\end{abstract} |
|
204 |
|
205 |
|
206 |
200 \addchaptertocentry{\abstractname} % Add the abstract to the table of contents |
207 \addchaptertocentry{\abstractname} % Add the abstract to the table of contents |
|
208 \addchap{Abstract} |
201 This work is about regular expressions and derivatives. It combines functional algorithms and their formal verification in the Isabelle/HOL theorem prover. |
209 This work is about regular expressions and derivatives. It combines functional algorithms and their formal verification in the Isabelle/HOL theorem prover. |
202 |
210 |
203 Theoretical results say that regular expression matching |
211 Theoretical results say that regular expression matching |
204 should be linear with respect to the input. |
212 should be linear with respect to the input. |
205 Under a certain class of regular expressions and inputs though, |
213 Under a certain class of regular expressions and inputs though, |
225 The result is an algorithm with provable guarantees on |
233 The result is an algorithm with provable guarantees on |
226 correctness and running time. We believe this is the first |
234 correctness and running time. We believe this is the first |
227 work with these two guarantees together. |
235 work with these two guarantees together. |
228 |
236 |
229 |
237 |
230 |
238 |
231 \end{abstract} |
|
232 |
239 |
233 %---------------------------------------------------------------------------------------- |
240 %---------------------------------------------------------------------------------------- |
234 % ACKNOWLEDGEMENTS |
241 % ACKNOWLEDGEMENTS |
235 %---------------------------------------------------------------------------------------- |
242 %---------------------------------------------------------------------------------------- |
236 |
243 |
358 % Uncomment the lines as you write the chapters |
365 % Uncomment the lines as you write the chapters |
359 |
366 |
360 \include{Chapters/Chapter1} |
367 \include{Chapters/Chapter1} |
361 \include{Chapters/Chapter2} |
368 \include{Chapters/Chapter2} |
362 \include{Chapters/Chapter3} |
369 \include{Chapters/Chapter3} |
363 %\include{Chapters/Chapter4} |
370 \include{Chapters/Chapter4} |
364 %\include{Chapters/Chapter5} |
371 \include{Chapters/Chapter5} |
365 |
372 |
366 %---------------------------------------------------------------------------------------- |
373 %---------------------------------------------------------------------------------------- |
367 % THESIS CONTENT - APPENDICES |
374 % THESIS CONTENT - APPENDICES |
368 %---------------------------------------------------------------------------------------- |
375 %---------------------------------------------------------------------------------------- |
369 |
376 |