%% This BibTeX bibliography file was created using BibDesk.

%% https://bibdesk.sourceforge.io/

%% Created for CS TAN at 2022-11-20 17:26:32 +0000 

%% Saved with string encoding Unicode (UTF-8) 

@inproceedings{Doczkal2013,

author = {C.~Doczkaland J.O.~Kaiser and G.~Smolka},

title = {A Constructive Theory of Regular Languages in Coq},

year = {2013},

isbn = {9783319035444},

publisher = {Springer-Verlag},

address = {Berlin, Heidelberg},

url = {https://doi.org/10.1007/978-3-319-03545-1_6},

doi = {10.1007/978-3-319-03545-1_6},

abstract = {We present a formal constructive theory of regular languages consisting of about 1400 lines of Coq/Ssreflect. As representations we consider regular expressions, deterministic and nondeterministic automata, and Myhill and Nerode partitions. We construct computable functions translating between these representations and show that equivalence of representations is decidable. We also establish the usual closure properties, give a minimization algorithm for DFAs, and prove that minimal DFAs are unique up to state renaming. Our development profits much from Ssreflect's support for finite types and graphs.},

booktitle = {Proceedings of the Third International Conference on Certified Programs and Proofs - Volume 8307},

pages = {82–97},

numpages = {16},

keywords = {finite automata, regular expressions, Myhill-Nerode, Ssreflect, Coq, regular languages}

}

@inproceedings{Lammich2012,

author = {P.~Lammichand T.~Tuerk},

year = {2012},

month = {08},

pages = {166-182},

title = {Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm},

isbn = {978-3-642-32346-1},

doi = {10.1007/978-3-642-32347-8_12}

}

@article{Krauss2012,

	author={A.~Krauss and T.~Nipkow},

title={Proof Pearl: Regular Expression Equivalence and Relation Algebra},

journal={J. Automated Reasoning},volume=49,pages={95--106},year=2012,note={published online March 2011}}

@article{kleene1956,

  title={Representation of events in nerve nets and finite automata},

  author={S.C.~Kleene and others},

  journal={Automata studies},

  volume={34},

  pages={3--41},

  year={1956},

  publisher={Princeton, NJ}

}

@inproceedings{Paulson2015,

	author = {L.~C.~Paulson},

	booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)},

	pages = {231--245},

	series = {LNAI},

	title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets},

	volume = {9195},

	year = {2015}}

@article{Murugesan2014,

	author = {N.~Murugesan and O.~V.~Shanmuga Sundaram},

	journal = {International Journal of Computer Trends and Technology},

	number = {1},

	pages = {29--33},

	title = {{S}ome {P}roperties of {B}rzozowski {D}erivatives of {R}egular {E}xpressions},

	url = {http://arxiv.org/abs/1407.5902},

	volume = {13},

	year = {2014},

	bdsk-url-1 = {http://arxiv.org/abs/1407.5902}}

@phdthesis{Ausaf,

	author = {F.~Ausaf},

	school = {King's College London},

	title = {{V}erified {L}exing and {P}arsing},

	year = {2018}}

@inproceedings{Okui10,

	abstract = {This paper offers a new efficient regular expression matching algorithm which follows the POSIX-type leftmost-longest rule. The algorithm basically emulates the subset construction without backtracking, so that its computational cost even in the worst case does not explode exponentially; the time complexity of the algorithm is O(mn(n{\thinspace}+{\thinspace}c)), where m is the length of a given input string, n the number of occurrences of the most frequently used letter in a given regular expression and c the number of subexpressions to be used for capturing substrings. A formalization of the leftmost-longest semantics by using parse trees is also discussed.},

	address = {Berlin, Heidelberg},

	author = {S.~Okui and T.~Suzuki},

	booktitle = {Implementation and Application of Automata},

	editor = {Domaratzki, Michael and Salomaa, Kai},

	isbn = {978-3-642-18098-9},

	pages = {231--240},

	publisher = {Springer Berlin Heidelberg},

	title = {Disambiguation in Regular Expression Matching via Position Automata with Augmented Transitions},

	year = {2011}}

@article{Berglund14,

	author = {M.~Berglund, F.~Drewes and B.~Van Der Merwe},

	doi = {10.4204/EPTCS.151.7},

	journal = {Electronic Proceedings in Theoretical Computer Science},

	month = {05},

	title = {Analyzing Catastrophic Backtracking Behavior in Practical Regular Expression Matching},

	volume = {151},

	year = {2014},

	bdsk-url-1 = {https://doi.org/10.4204/EPTCS.151.7}}

@inproceedings{Berglund18,

	abstract = {Whereas Perl-compatible regular expression matchers typically exhibit some variation of leftmost-greedy semantics, those conforming to the posix standard are prescribed leftmost-longest semantics. However, the posix standard leaves some room for interpretation, and Fowler and Kuklewicz have done experimental work to confirm differences between various posix matchers. The Boost library has an interesting take on the posix standard, where it maximises the leftmost match not with respect to subexpressions of the regular expression pattern, but rather, with respect to capturing groups. In our work, we provide the first formalisation of Boost semantics, and we analyse the complexity of regular expression matching when using Boost semantics.},

	address = {Cham},

	author = {M.~Berglund and W.~Bester and B.~Van Der Merwe},

	booktitle = {Theoretical Aspects of Computing -- ICTAC 2018},

	editor = {Fischer, Bernd and Uustalu, Tarmo},

	isbn = {978-3-030-02508-3},

	pages = {99--115},

	publisher = {Springer International Publishing},

	title = {Formalising Boost POSIX Regular Expression Matching},

	year = {2018}}

@inproceedings{Chen12,

	author = {H.~Chenand S.~Yu},

	doi = {10.1007/978-3-642-27654-5_27},

	month = {01},

	pages = {343-356},

	title = {Derivatives of Regular Expressions and an Application},

	volume = {7160},

	year = {2012},

	bdsk-url-1 = {https://doi.org/10.1007/978-3-642-27654-5_27}}

@article{Takayuki2019,

	author = {T.~Miyazaki and Y.~Minamide},

	doi = {10.2197/ipsjjip.27.422},

	journal = {Journal of Information Processing},

	pages = {422-430},

	title = {Derivatives of Regular Expressions with Lookahead},

	volume = {27},

	year = {2019},

	bdsk-url-1 = {https://doi.org/10.2197/ipsjjip.27.422}}

@article{FERNAU2015287,

	abstract = {A pattern α, i.e., a string that contains variables and terminals, matches a terminal word w if w can be obtained by uniformly substituting the variables of α by terminal words. Deciding whether a given terminal word matches a given pattern is NP-complete and this holds for several natural variants of the problem that result from whether or not variables can be erased, whether or not the patterns are required to be terminal-free or whether or not the mapping of variables to terminal words must be injective. We consider numerous parameters of this problem (i.e., number of variables, length of w, length of the words substituted for variables, number of occurrences per variable, cardinality of the terminal alphabet) and for all possible combinations of the parameters (and variants described above), we answer the question whether or not the problem is still NP-complete if these parameters are bounded by constants.},

	author = {H.~Fernau and M.L.~Schmid},

	doi = {https://doi.org/10.1016/j.ic.2015.03.006},

	issn = {0890-5401},

	journal = {Information and Computation},

	keywords = {Parameterised pattern matching, Function matching, NP-completeness, Membership problem for pattern languages, Morphisms},

	pages = {287-305},

	title = {Pattern matching with variables: A multivariate complexity analysis},

	url = {https://www.sciencedirect.com/science/article/pii/S0890540115000218},

	volume = {242},

	year = {2015},

	bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0890540115000218},

	bdsk-url-2 = {https://doi.org/10.1016/j.ic.2015.03.006}}

@inproceedings{Schmid2012,

	abstract = {We study different possibilities of combining the concept of homomorphic replacement with regular expressions in order to investigate the class of languages given by extended regular expressions with backreferences (REGEX). It is shown in which regard existing and natural ways to do this fail to reach the expressive power of REGEX. Furthermore, the complexity of the membership problem for REGEX with a bounded number of backreferences is considered.},

	address = {Berlin, Heidelberg},

	author = {M.L.~Schmid},

	booktitle = {Proceedings of the 16th International Conference on Developments in Language Theory},

	doi = {10.1007/978-3-642-31653-1_8},

	isbn = {9783642316524},

	keywords = {extended regular expressions, pattern languages, REGEX, pattern expressions, homomorphic replacement},

	location = {Taipei, Taiwan},

	numpages = {12},

	pages = {73--84},

	publisher = {Springer-Verlag},

	series = {DLT'12},

	title = {Inside the Class of REGEX Languages},

	url = {https://doi.org/10.1007/978-3-642-31653-1_8},

	year = {2012},

	bdsk-url-1 = {https://doi.org/10.1007/978-3-642-31653-1_8}}

@article{BERGLUND2022,

	abstract = {Most modern regular expression matching libraries (one of the rare exceptions being Google's RE2) allow backreferences, operations which bind a substring to a variable, allowing it to be matched again verbatim. However, both real-world implementations and definitions in the literature use different syntactic restrictions and have differences in the semantics of the matching of backreferences. Our aim is to compare these various flavors by considering the classes of formal languages that each can describe, establishing, as a result, a hierarchy of language classes. Beyond the hierarchy itself, some complexity results are given, and as part of the effort on comparing language classes new pumping lemmas are established, old classes are extended to new ones, and several incidental results on the nature of these language classes are given.},

	author = {M.~Berglund and B.~Van Der Merwe},

	doi = {https://doi.org/10.1016/j.tcs.2022.10.041},

	issn = {0304-3975},

	journal = {Theoretical Computer Science},

	keywords = {Regular expressions, Backreferences},

	title = {Re-examining regular expressions with backreferences},

	url = {https://www.sciencedirect.com/science/article/pii/S0304397522006570},

	year = {2022},

	bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397522006570},

	bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2022.10.041}}

@article{FREYDENBERGER20191,

	abstract = {Most modern libraries for regular expression matching allow back-references (i.e., repetition operators) that substantially increase expressive power, but also lead to intractability. In order to find a better balance between expressiveness and tractability, we combine these with the notion of determinism for regular expressions used in XML DTDs and XML Schema. This includes the definition of a suitable automaton model, and a generalization of the Glushkov construction. We demonstrate that, compared to their non-deterministic superclass, these deterministic regular expressions with back-references have desirable algorithmic properties (i.e., efficiently solvable membership problem and some decidable problems in static analysis), while, at the same time, their expressive power exceeds that of deterministic regular expressions without back-references.},

	author = {D.D.~Freydenberger and M.L.~Schmid},

	doi = {https://doi.org/10.1016/j.jcss.2019.04.001},

	issn = {0022-0000},

	journal = {Journal of Computer and System Sciences},

	keywords = {Deterministic regular expression, Regex, Glushkov automaton},

	pages = {1-39},

	title = {Deterministic regular expressions with back-references},

	url = {https://www.sciencedirect.com/science/article/pii/S0022000018301818},

	volume = {105},

	year = {2019},

	bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0022000018301818},

	bdsk-url-2 = {https://doi.org/10.1016/j.jcss.2019.04.001}}

@inproceedings{Frey2013,

	address = {Dagstuhl, Germany},

	annote = {Keywords: extended regular expressions, regex, decidability, non-recursive tradeoffs},

	author = {D.D.~Freydenberger},

	booktitle = {28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)},

	doi = {10.4230/LIPIcs.STACS.2011.507},

	editor = {Thomas Schwentick and Christoph D{\"u}rr},

	isbn = {978-3-939897-25-5},

	issn = {1868-8969},

	pages = {507--518},

	publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},

	series = {Leibniz International Proceedings in Informatics (LIPIcs)},

	title = {{Extended Regular Expressions: Succinctness and Decidability}},

	url = {http://drops.dagstuhl.de/opus/volltexte/2011/3039},

	urn = {urn:nbn:de:0030-drops-30396},

	volume = {9},

	year = {2011},

	bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2011/3039},

	bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.STACS.2011.507}}

@article{campeanu2003formal,

	author = {C.~C{\^a}mpeanu and K.~Salomaa and S.~Yu},

	journal = {International Journal of Foundations of Computer Science},

	number = {06},

	pages = {1007--1018},

	publisher = {World Scientific},

	title = {A formal study of practical regular expressions},

	volume = {14},

	year = {2003}}

@article{campeanu2009patterns,

	author = {C.~C{\^a}mpeanu and N.~Santean},

	doi = {10.1007/s00236-009-0090-y},

	journal = {Acta Inf.},

	month = {05},

	pages = {193-207},

	title = {On the closure of pattern expressions languages under intersection with regular languages},

	volume = {46},

	year = {2009},

	bdsk-url-1 = {https://doi.org/10.1007/s00236-009-0090-y}}

@article{CAMPEANU2009Intersect,

	abstract = {In this paper we revisit the semantics of extended regular expressions (regex), defined succinctly in the 90s [A.V. Aho, Algorithms for finding patterns in strings, in: Jan van Leeuwen (Ed.), Handbook of Theoretical Computer Science, in: Algorithms and Complexity, vol. A, Elsevier and MIT Press, 1990, pp. 255--300] and rigorously in 2003 by C{\^a}mpeanu, Salomaa and Yu [C. C{\^a}mpeanu, K. Salomaa, S. Yu, A formal study of practical regular expressions, IJFCS 14 (6) (2003) 1007--1018], when the authors reported an open problem, namely whether regex languages are closed under the intersection with regular languages. We give a positive answer; and for doing so, we propose a new class of machines --- regex automata systems (RAS) --- which are equivalent to regex. Among others, these machines provide a consistent and convenient method of implementing regex in practice. We also prove, as a consequence of this closure property, that several languages, such as the mirror language, the language of palindromes, and the language of balanced words are not regex languages.},

	author = {C.~C{\^a}mpeanu and N.~Santean},

	doi = {https://doi.org/10.1016/j.tcs.2009.02.022},

	issn = {0304-3975},

	journal = {Theoretical Computer Science},

	keywords = {Extended regular expression, Regex automata system, Regex},

	note = {Formal Languages and Applications: A Collection of Papers in Honor of Sheng Yu},

	number = {24},

	pages = {2336-2344},

	title = {On the intersection of regex languages with regular languages},

	url = {https://www.sciencedirect.com/science/article/pii/S0304397509001789},

	volume = {410},

	year = {2009},

	bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397509001789},

	bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2009.02.022}}

@incollection{Aho1990,

	abstract = {Publisher Summary

This chapter discusses the algorithms for solving string-matching problems that have proven useful for text-editing and text-processing applications. String pattern matching is an important problem that occurs in many areas of science and information processing. In computing, it occurs naturally as part of data processing, text editing, term rewriting, lexical analysis, and information retrieval. Many text editors and programming languages have facilities for matching strings. In biology, string-matching problems arise in the analysis of nucleic acids and protein sequences, and in the investigation of molecular phylogeny. String matching is also one of the central and most widely studied problems in theoretical computer science. The simplest form of the problem is to locate an occurrence of a keyword as a substring in a sequence of characters, which is called the input string. For example, the input string queueing contains the keyword ueuei as a substring. Even for this problem, several innovative, theoretically interesting algorithms have been devised that run significantly faster than the obvious brute-force method.},

	address = {Amsterdam},

	author = {A.V.~Aho},

	booktitle = {Algorithms and Complexity},

	doi = {https://doi.org/10.1016/B978-0-444-88071-0.50010-2},

	editor = {JAN {VAN LEEUWEN}},

	isbn = {978-0-444-88071-0},

	pages = {255-300},

	publisher = {Elsevier},

	series = {Handbook of Theoretical Computer Science},

	title = {CHAPTER 5 - Algorithms for Finding Patterns in Strings},

	url = {https://www.sciencedirect.com/science/article/pii/B9780444880710500102},

	year = {1990},

	bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/B9780444880710500102},

	bdsk-url-2 = {https://doi.org/10.1016/B978-0-444-88071-0.50010-2}}

@inproceedings{Might2011,

	abstract = {We present a functional approach to parsing unrestricted context-free grammars based on Brzozowski's derivative of regular expressions. If we consider context-free grammars as recursive regular expressions, Brzozowski's equational theory extends without modification to context-free grammars (and it generalizes to parser combinators). The supporting actors in this story are three concepts familiar to functional programmers - laziness, memoization and fixed points; these allow Brzozowski's original equations to be transliterated into purely functional code in about 30 lines spread over three functions.Yet, this almost impossibly brief implementation has a drawback: its performance is sour - in both theory and practice. The culprit? Each derivative can double the size of a grammar, and with it, the cost of the next derivative.Fortunately, much of the new structure inflicted by the derivative is either dead on arrival, or it dies after the very next derivative. To eliminate it, we once again exploit laziness and memoization to transliterate an equational theory that prunes such debris into working code. Thanks to this compaction, parsing times become reasonable in practice.We equip the functional programmer with two equational theories that, when combined, make for an abbreviated understanding and implementation of a system for parsing context-free languages.},

	address = {New York, NY, USA},

	author = {M.~Might and D.~Darais and D.~Spiewak},

	booktitle = {Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming},

	doi = {10.1145/2034773.2034801},

	isbn = {9781450308656},

	keywords = {derivative, parsing, context-free grammar, parser combinator, formal languages, regular expressions},

	location = {Tokyo, Japan},

	numpages = {7},

	pages = {189--195},

	publisher = {Association for Computing Machinery},

	series = {ICFP '11},

	title = {Parsing with Derivatives: A Functional Pearl},

	url = {https://doi.org/10.1145/2034773.2034801},

	year = {2011},

	bdsk-url-1 = {https://doi.org/10.1145/2034773.2034801}}

@inproceedings{Adams2016,

  title={On the complexity and performance of parsing with derivatives},

  author={M.D.~Adams and C.~Hollenbeck and M.~MightMatthew},

  booktitle={Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation},

  pages={224--236},

  year={2016}

}

@article{Huet1997,

author = {G.~Huet},

title = {The Zipper},

year = {1997},

issue_date = {September 1997},

publisher = {Cambridge University Press},

address = {USA},

volume = {7},

number = {5},

issn = {0956-7968},

url = {https://doi.org/10.1017/S0956796897002864},

doi = {10.1017/S0956796897002864},

abstract = {Almost every programmer has faced the problem of representing a tree together with a subtree that is the focus of attention, where that focus may move left, right, up or down the tree. The Zipper is Huet's nifty name for a nifty data structure which fulfills this need. I wish I had known of it when I faced this task, because the solution I came up with was not quite so efficient or elegant as the Zipper.},

journal = {J. Funct. Program.},

month = {sep},

pages = {549–554},

numpages = {6}

}

@article{Darragh2020,

	abstract = {Parsing with Derivatives (PwD) is an elegant approach to parsing context-free grammars (CFGs). It takes the equational theory behind Brzozowski's derivative for regular expressions and augments that theory with laziness, memoization, and fixed points. The result is a simple parser for arbitrary CFGs. Although recent work improved the performance of PwD, it remains inefficient due to the algorithm repeatedly traversing some parts of the grammar. In this functional pearl, we show how to avoid this inefficiency by suspending the state of the traversal in a zipper. When subsequent derivatives are taken, we can resume the traversal from where we left off without retraversing already traversed parts of the grammar. However, the original zipper is designed for use with trees, and we want to parse CFGs. CFGs can include shared regions, cycles, and choices between alternates, which makes them incompatible with the traditional tree model for zippers. This paper develops a generalization of zippers to properly handle these additional features. Just as PwD generalized Brzozowski's derivatives from regular expressions to CFGs, we generalize Huet's zippers from trees to CFGs. Abstract The resulting parsing algorithm is concise and efficient: it takes only 31 lines of OCaml code to implement the derivative function but performs 6,500 times faster than the original PwD and 3.24 times faster than the optimized implementation of PwD.},

	address = {New York, NY, USA},

	articleno = {108},

	author = {P.~Darragh and M.D.~Adams},

	doi = {10.1145/3408990},

	issue_date = {August 2020},

	journal = {Proc. ACM Program. Lang.},

	keywords = {Derivatives, Zippers, Parsing with Derivatives, Parsing},

	month = {aug},

	number = {ICFP},

	numpages = {28},

	publisher = {Association for Computing Machinery},

	title = {Parsing with Zippers (Functional Pearl)},

	url = {https://doi.org/10.1145/3408990},

	volume = {4},

	year = {2020},

	bdsk-url-1 = {https://doi.org/10.1145/3408990}}

@article{Edelmann2021,

	abstract = {Parsing is the process that enables a computer system to  make sense of raw data. Parsing is common to almost all  computer systems: It is involved every time sequential data  is read and elaborated into structured data. The theory of  parsing usually focuses on the binary recognition aspect of  parsing and eschews this essential data-elaboration aspect.  In this thesis, I present a declarative framework for  value-aware parsing that explicitly integrates data  elaboration.

Within the framework of the thesis, I present  parsing algorithms that are based on the concept of  Brzozowski's derivatives. Derivative-based parsing  algorithms present several advantages: they are elegant,  amenable to formal reasoning, and easy to implement.  Unfortunately, the performance of these algorithms in  practice is often not competitive with other approaches. In  this thesis, I show a general technique inspired by Huet's  Zipper to greatly enhance the performance of  derivative-based algorithms, and I do so without  compromising their elegance, amenability to formal  reasoning, or ease of implementation.

First, I present a  technique for building efficient tokenisers that is based  on Brzozowski's derivatives and Huet's zipper and that does  not require the usual burdensome explicit conversion to  automata. I prove the technique is correct in Coq and  present SILEX, a Scala lexing library based on the  technique. I demonstrate that the approach is competitive  with state-of-the-art solutions.

Then, I present a  characterisation of LL(1) languages based on the concept of  should-not-follow sets. I present an algorithm for parsing  LL(1) languages with derivatives and zippers. I show a  formal proof of the algorithm's correctness and prove its  worst-case linear-time complexity. I show how the LL(1)  parsing with derivatives and zippers algorithm corresponds  to the traditional LL(1) parsing algorithm.

I then present  SCALL1ON, a Scala parsing combinators library for LL(1)  languages that incorporates the LL(1) parsing with  derivatives and zippers algorithm. I present an expressive  and familiar combinator-based interface for describing  LL(1) languages. I present techniques that help precisely  locate LL(1) conflicts in user code. I discuss several  advantages of the parsing with derivatives approach within  the context of a parsing library. I also present SCALL1ON's  enumeration and pretty-printing features and discuss their  implementation. Through a series of benchmarks, I  demonstrate the good performance and practicality of the  approach. Finally, I present how to adapt the LL(1) parsing  with derivatives and zippers algorithm to support arbitrary  context-free languages. I show how the adapted algorithm  corresponds to general parsing algorithms, such as Earley's  parsing algorithm.},

	address = {Lausanne},

	author = {R.~Edelmann},

	doi = {10.5075/epfl-thesis-7357},

	institution = {IINFCOM},

	pages = {246},

	publisher = {EPFL},

	title = {Efficient Parsing with Derivatives and Zippers},

	url = {http://infoscience.epfl.ch/record/287059},

	year = {2021},

	bdsk-url-1 = {http://infoscience.epfl.ch/record/287059},

	bdsk-url-2 = {https://doi.org/10.5075/epfl-thesis-7357}}

@inproceedings{Zippy2020,

	abstract = {In this paper, we present an efficient, functional, and formally verified parsing algorithm for LL(1) context-free expressions based on the concept of derivatives of formal languages. Parsing with derivatives is an elegant parsing technique, which, in the general case, suffers from cubic worst-case time complexity and slow performance in practice. We specialise the parsing with derivatives algorithm to LL(1) context-free expressions, where alternatives can be chosen given a single token of lookahead. We formalise the notion of LL(1) expressions and show how to efficiently check the LL(1) property. Next, we present a novel linear-time parsing with derivatives algorithm for LL(1) expressions operating on a zipper-inspired data structure. We prove the algorithm correct in Coq and present an implementation as a part of Scallion, a parser combinators framework in Scala with enumeration and pretty printing capabilities.},

	address = {New York, NY, USA},

	author = {R.~Edelmann and H.~Jad and K.~Viktor},

	booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},

	doi = {10.1145/3385412.3385992},

	isbn = {9781450376136},

	keywords = {Parsing, Zipper, Formal proof, LL(1), Derivatives},

	location = {London, UK},

	numpages = {16},

	pages = {1036--1051},

	publisher = {Association for Computing Machinery},

	series = {PLDI 2020},

	title = {Zippy LL(1) Parsing with Derivatives},

	url = {https://doi.org/10.1145/3385412.3385992},

	year = {2020},

	bdsk-url-1 = {https://doi.org/10.1145/3385412.3385992}}

@article{fowler2003,

	author = {G.~Fowler},

	journal = {URL: https://web. archive. org/web/20050408073627/http://www. research. att. com/\~{} gsf/testregex/re-interpretation. html},

	title = {An interpretation of the POSIX regex standard},

	year = {2003}}

@inproceedings{Snort1999,

	abstract = {Network intrusion detection systems (NIDS) are an important part of any network security architecture. They provide a layer of defense which monitors network traffic for predefined suspicious activity or patterns, and alert system administrators when potential hostile traffic is detected. Commercial NIDS have many differences, but Information Systems departments must face the commonalities that they share such as significant system footprint, complex deployment and high monetary cost. Snort was designed to address these issues.},

	address = {USA},

	author = {M.~Roesch},

	booktitle = {Proceedings of the 13th USENIX Conference on System Administration},

	location = {Seattle, Washington},

	numpages = {10},

	pages = {229--238},

	publisher = {USENIX Association},

	series = {LISA '99},

	title = {Snort - Lightweight Intrusion Detection for Networks},

	year = {1999}}

@article{Reps1998,

author = {T.~Reps},

title = {“Maximal-Munch” Tokenization in Linear Time},

year = {1998},

issue_date = {March 1998},

publisher = {Association for Computing Machinery},

address = {New York, NY, USA},

volume = {20},

number = {2},

issn = {0164-0925},

url = {https://doi.org/10.1145/276393.276394},

doi = {10.1145/276393.276394},

abstract = {The lexical-analysis (or scanning) phase of a compiler attempts to partition an input string into a sequence of tokens. The convention in most languages is that the input is scanned left to right, and each token identified is a “maximal munch” of the remaining input—the longest prefix of the remaining input that is a token of the language. Although most of the standard compiler textbooks present a way to perform maximal-munch tokenization, the algorithm they describe is one that, for certain sets of token definitions, can cause the scanner to exhibit quadratic behavior in the worst case. In the article, we show that maximal-munch tokenization can always be performed in time linear in the size of the input.},

journal = {ACM Trans. Program. Lang. Syst.},

month = {mar},

pages = {259–273},

numpages = {15},

keywords = {backtracking, tokenization, tabulation, dynamic programming, memoization}

}

@inproceedings{Bro,

author = {V.~Paxson},

title = {Bro: A System for Detecting Network Intruders in Real-Time},

year = {1998},

publisher = {USENIX Association},

address = {USA},

abstract = {We describe Bro, a stand-alone system for detecting network intruders in real-time by passively monitoring a network link over which the intruder's traffic transits. We give an overview of the system's design, which emphasizes high-speed (FDDI-rate) monitoring, real-time notification, clear separation between mechanism and policy, and extensibility. To achieve these ends, Bro is divided into an "event engine" that reduces a kernel-filtered network traffic stream into a series of higher-level events, and a "policy script interpreter" that interprets event handlers written in a specialized language used to express a site's security policy. Event handlers can update state information, synthesize new events, record information to disk, and generate real-time notifications via syslog. We also discuss a number of attacks that attempt to subvert passive monitoring systems and defenses against these, and give particulars of how Bro analyzes the four applications integrated into it so far: Finger, FTP, Portmapper and Telnet. The system is publicly available in source code form.},

booktitle = {Proceedings of the 7th Conference on USENIX Security Symposium - Volume 7},

pages = {3},

numpages = {1},

location = {San Antonio, Texas},

series = {SSYM'98}

}

@INPROCEEDINGS{Sidhu2001,

  author={R.~Sidhu and V.K.~Prasanna},

  booktitle={The 9th Annual IEEE Symposium on Field-Programmable Custom Computing Machines (FCCM'01)}, 

  title={Fast Regular Expression Matching Using FPGAs}, 

  year={2001},

  volume={},

  number={},

  pages={227-238},

  doi={}

}

@article{Turonova2020,

author = {L.~Turo\v{n}ov\'{a} and L.~Hol\'{\i}k  and O.~Leng\'{a}l and O.~Saarikivi and M.~Veanes and T.~Vojnar },

title = {Regex Matching with Counting-Set Automata},

year = {2020},

issue_date = {November 2020},

publisher = {Association for Computing Machinery},

address = {New York, NY, USA},

volume = {4},

number = {OOPSLA},

url = {https://doi.org/10.1145/3428286},

doi = {10.1145/3428286},

abstract = {We propose a solution to the problem of efficient matching regular expressions (regexes) with bounded repetition, such as (ab){1,100}, using deterministic automata. For this, we introduce novel counting-set automata (CsAs), automata with registers that can hold sets of bounded integers and can be manipulated by a limited portfolio of constant-time operations. We present an algorithm that compiles a large sub-class of regexes to deterministic CsAs. This includes (1) a novel Antimirov-style translation of regexes with counting to counting automata (CAs), nondeterministic automata with bounded counters, and (2) our main technical contribution, a determinization of CAs that outputs CsAs. The main advantage of this workflow is that the size of the produced CsAs does not depend on the repetition bounds used in the regex (while the size of the DFA is exponential to them). Our experimental results confirm that deterministic CsAs produced from practical regexes with repetition are indeed vastly smaller than the corresponding DFAs. More importantly, our prototype matcher based on CsA simulation handles practical regexes with repetition regardless of sizes of counter bounds. It easily copes with regexes with repetition where state-of-the-art matchers struggle.},

journal = {Proc. ACM Program. Lang.},

month = {nov},

articleno = {218},

numpages = {30},

keywords = {counting-set automata, counting automata, bounded repetition, ReDos, Antimirov's derivatives, regular expression matching, determinization}

}

@inproceedings{Kumar2006,

author = {S.~Kumar and S.~Dharmapurikar and F.~Yu and P.~Crowley and J.~Turner},

title = {Algorithms to Accelerate Multiple Regular Expressions Matching for Deep Packet Inspection},

year = {2006},

isbn = {1595933085},

publisher = {Association for Computing Machinery},

address = {New York, NY, USA},

url = {https://doi.org/10.1145/1159913.1159952},

doi = {10.1145/1159913.1159952},

abstract = {There is a growing demand for network devices capable of examining the content of data packets in order to improve network security and provide application-specific services. Most high performance systems that perform deep packet inspection implement simple string matching algorithms to match packets against a large, but finite set of strings. owever, there is growing interest in the use of regular expression-based pattern matching, since regular expressions offer superior expressive power and flexibility. Deterministic finite automata (DFA) representations are typically used to implement regular expressions. However, DFA representations of regular expression sets arising in network applications require large amounts of memory, limiting their practical application.In this paper, we introduce a new representation for regular expressions, called the Delayed Input DFA (D2FA), which substantially reduces space equirements as compared to a DFA. A D2FA is constructed by transforming a DFA via incrementally replacing several transitions of the automaton with a single default transition. Our approach dramatically reduces the number of distinct transitions between states. For a collection of regular expressions drawn from current commercial and academic systems, a D2FA representation reduces transitions by more than 95%. Given the substantially reduced space equirements, we describe an efficient architecture that can perform deep packet inspection at multi-gigabit rates. Our architecture uses multiple on-chip memories in such a way that each remains uniformly occupied and accessed over a short duration, thus effectively distributing the load and enabling high throughput. Our architecture can provide ostffective packet content scanning at OC-192 rates with memory requirements that are consistent with current ASIC technology.},

booktitle = {Proceedings of the 2006 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications},

pages = {339–350},

numpages = {12},

keywords = {regular expressions, DFA, deep packet inspection},

location = {Pisa, Italy},

series = {SIGCOMM '06}

}

@inproceedings{Becchi2007,