ChengsongTanPhdThesis/main.tex
changeset 527 2c907b118f78
parent 526 cb702fb4227f
child 528 28751de4b4ba
equal deleted inserted replaced
526:cb702fb4227f 527:2c907b118f78
   201 
   201 
   202  
   202  
   203 %\end{abstract}
   203 %\end{abstract}
   204 
   204 
   205 
   205 
   206 
   206 \begin{abstract}
   207 \addchaptertocentry{\abstractname} % Add the abstract to the table of contents
   207 \addchaptertocentry{\abstractname} % Add the abstract to the table of contents
   208 \addchap{Abstract} 
   208 %\addchap{Abstract} 
   209 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.
   210 
   210 
   211 Theoretical results say that regular expression matching
   211 Theoretical results say that regular expression matching
   212 should be linear with respect to the input.
   212 should be linear with respect to the input.
   213 Under a certain class of regular expressions and inputs though,
   213 Under a certain class of regular expressions and inputs though,
   231 Antimirov.
   231 Antimirov.
   232 The result is an algorithm with provable guarantees on 
   232 The result is an algorithm with provable guarantees on 
   233 correctness and running time. We believe this is the first 
   233 correctness and running time. We believe this is the first 
   234 work with these two guarantees together.
   234 work with these two guarantees together.
   235 
   235 
   236 
   236 \end{abstract}
   237 
   237 
   238 
   238 
   239 %----------------------------------------------------------------------------------------
   239 %----------------------------------------------------------------------------------------
   240 %	ACKNOWLEDGEMENTS
   240 %	ACKNOWLEDGEMENTS
   241 %----------------------------------------------------------------------------------------
   241 %----------------------------------------------------------------------------------------
   363 % Include the chapters of the thesis as separate files from the Chapters folder
   363 % Include the chapters of the thesis as separate files from the Chapters folder
   364 % Uncomment the lines as you write the chapters
   364 % Uncomment the lines as you write the chapters
   365 
   365 
   366 \include{Chapters/Chapter1}
   366 \include{Chapters/Chapter1}
   367 \include{Chapters/Chapter2} 
   367 \include{Chapters/Chapter2} 
   368 \include{Chapters/Chapter3}
   368 \include{Chapters/ChapterBitcoded1}
   369 \include{Chapters/Chapter4} 
   369 \include{Chapters/ChapterBitcoded2}
       
   370 \include{Chapters/ChapterFinite} 
   370 \include{Chapters/Chapter5} 
   371 \include{Chapters/Chapter5} 
       
   372 \include{Chapters/Chapter6}
   371 
   373 
   372 %----------------------------------------------------------------------------------------
   374 %----------------------------------------------------------------------------------------
   373 %	THESIS CONTENT - APPENDICES
   375 %	THESIS CONTENT - APPENDICES
   374 %----------------------------------------------------------------------------------------
   376 %----------------------------------------------------------------------------------------
   375 
   377