--- a/ChengsongTanPhdThesis/example.bib Tue Jul 25 17:28:29 2023 +0100
+++ b/ChengsongTanPhdThesis/example.bib Wed Aug 23 03:02:31 2023 +0100
@@ -2,8 +2,21 @@
%% https://bibdesk.sourceforge.io/
%% Created for CS TAN at 2022-11-20 17:26:32 +0000
-
-
+@inproceedings{LEX,
+ title={Lex—a lexical analyzer generator},
+ author={Michael E. Lesk and Eric E. Schmidt},
+ year={1990},
+ url={https://api.semanticscholar.org/CorpusID:7900881}
+}
+@article{RegularExpressions,
+ title={REPRESENTATION OF EVENTS IN NERVE NETS AND FINITE AUTOMATA$^1$},
+ author={Kleene, SC},
+ journal={Automata Studies: Annals of Mathematics Studies. Number 34},
+ number={34},
+ pages={3},
+ year={1956},
+ publisher={Princeton University Press}
+}
%% Saved with string encoding Unicode (UTF-8)
@inproceedings{Doczkal2013,
author = {C.~Doczkaland J.O.~Kaiser and G.~Smolka},
@@ -684,6 +697,38 @@
title = {{Snort Community Rules}},
year = {2022}}
+@misc{Atom,
+ howpublished = {\url{https://github.com/atom/atom}},
+ note = {[Online; last accessed 22-Aug-2023]},
+ title = {{Atom Editor}},
+ year = {2023}}
+
+@misc{fixedAtom,
+ howpublished = {\url{http://davidvgalbraith.com/how-i-fixed-atom/}},
+ note = {[Online; last accessed 22-Aug-2023}},
+ title = {{How I fixed Atom}},
+ year = {2016}}
+
+
+@misc{Cloudflare,
+ howpublished = {\url{https://www.cloudflare.com/en-gb/}},
+ note = {[Online; last accessed 22-Aug-2023}},
+ title = {{Cloudflare}},
+ year = {2023}}
+
+@misc{CloudflareOutage,
+ howpublished = {\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}},
+ note = {[Online; last accessed 22-Aug-2023}},
+ title = {{Cloudflare}},
+ year = {2023}}
+
+@misc{TwainRegex,
+ howpublished = {\url{https://zherczeg.github.io/sljit/regex_perf.html}},
+ %note = {[Online; last accessed 19-November-2022]},
+ author = {Zoltan Herczeg},
+ title = {{Performance comparison of regular expression engines}},
+ year = {2015}}
+
@misc{KuklewiczHaskell,
author = {C.~Kuklewicz},
keywords = {Buggy C POSIX Lexing Libraries},
@@ -857,6 +902,15 @@
volume = 1479,
year = 1998}
+@book{Isabelle,
+ title={Isabelle/HOL: a proof assistant for higher-order logic},
+ author={Nipkow, Tobias and Paulson, Lawrence C and Wenzel, Markus},
+ volume={2283},
+ year={2002},
+ publisher={Springer Science \& Business Media}
+}
+
+
@article{Brzozowski1964,
author = {J.~A.~Brzozowski},
journal = {Journal of the {ACM}},
@@ -1054,6 +1108,37 @@
abstract="We present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. We build on top of Separation Logic with Time Credits, embedded in an interactive proof assistant. We formalize the O notation, which is key to enabling modular specifications and proofs. We cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. We propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples.",
isbn="978-3-319-89884-1"
}
+
+
+@article{ValiantParsing,
+ title={General Context-Free Recognition in Less than Cubic Time},
+ author={Leslie G. Valiant},
+ journal={J. Comput. Syst. Sci.},
+ year={1975},
+ volume={10},
+ pages={308-315}
+}
+
+
+@inproceedings{bigOIsabelle,
+ title={Formalizing O notation in Isabelle/HOL},
+ author={Avigad, Jeremy and Donnelly, Kevin},
+ booktitle={International Joint Conference on Automated Reasoning},
+ pages={357--371},
+ year={2004},
+ organization={Springer}
+}
+
+
+@inbook{subtypingFormalComplexity,
+author = {Bessai, Jan and Rehof, Jakob and Düdder, Boris},
+year = {2019},
+month = {06},
+pages = {356-371},
+title = {Fast Verified BCD Subtyping},
+isbn = {978-3-030-22347-2},
+doi = {10.1007/978-3-030-22348-9_21}
+}
%@article{10.1145/640128.604148,
%author = {Hofmann, Martin and Jost, Steffen},
%title = {Static Prediction of Heap Space Usage for First-Order Functional Programs},
@@ -1093,3 +1178,23 @@
%}
+%10.1145/3591262,
+
+@article{Margus2023PLDI,
+author = {Moseley, Dan and Nishio, Mario and Perez Rodriguez, Jose and Saarikivi, Olli and Toub, Stephen and Veanes, Margus and Wan, Tiki and Xu, Eric},
+title = {Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics},
+year = {2023},
+issue_date = {June 2023},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {7},
+number = {PLDI},
+url = {https://doi.org/10.1145/3591262},
+doi = {10.1145/3591262},
+abstract = {We develop a new derivative based theory and algorithm for nonbacktracking regex matching that supports anchors and counting, preserves backtracking semantics, and can be extended with lookarounds. The algorithm has been implemented as a new regex backend in .NET and was extensively tested as part of the formal release process of .NET7. We present a formal proof of the correctness of the algorithm, which we believe to be the first of its kind concerning industrial implementations of regex matchers. The paper describes the complete foundation, the matching algorithm, and key aspects of the implementation involving a regex rewrite system, as well as a comprehensive evaluation over industrial case studies and other regex engines.},
+journal = {Proc. ACM Program. Lang.},
+month = {jun},
+articleno = {148},
+numpages = {24},
+keywords = {automata, derivative, symbolic, regex, PCRE, matching}
+}