%% This BibTeX bibliography file was created using BibDesk.

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

%% Created for CS TAN at 2022-05-23 18:43:50 +0100 

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

@article{Murugesan2014,

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

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

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

  volume    = {13},

  number    = {1},

  year      = {2014},

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

  pages     = {29--33}

}

@PhdThesis{Ausaf,

  author =       {F.~Ausaf},

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

  school =       {King's College London},

  year =         {2018}

}

%% POSIX specification------------------------

@InProceedings{Okui10,

author=" S.~Okui

and T.~Suzuki",

editor="Domaratzki, Michael

and Salomaa, Kai",

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

booktitle="Implementation and Application of Automata",

year="2011",

publisher="Springer Berlin Heidelberg",

address="Berlin, Heidelberg",

pages="231--240",

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.",

isbn="978-3-642-18098-9"

}

%% POSIX specification------------------------

%% Brzozowski ders------------------------

@article{Berglund14,

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

year = {2014},

month = {05},

pages = {},

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

volume = {151},

journal = {Electronic Proceedings in Theoretical Computer Science},

doi = {10.4204/EPTCS.151.7}

}

@InProceedings{Berglund18,

author="M.~Berglund

and Bester, Willem

and van der Merwe, Brink",

editor="Fischer, Bernd

and Uustalu, Tarmo",

title="Formalising Boost POSIX Regular Expression Matching",

booktitle="Theoretical Aspects of Computing -- ICTAC 2018",

year="2018",

publisher="Springer International Publishing",

address="Cham",

pages="99--115",

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.",

isbn="978-3-030-02508-3"

}

@inproceedings{Chen12,

author = {Chen, Haiming and Yu, Sheng},

year = {2012},

month = {01},

pages = {343-356},

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

volume = {7160},

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

}

%% Brzozowski ders------------------------

%@article{Murugesan2014,

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

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

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

%  volume    = {13},

%  number    = {1},

%  year      = {2014},

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

%  pages     = {29--33}

%}

%% look-aheads------------------------

@article{Takayuki2019,

  title={Derivatives of Regular Expressions with Lookahead},

  author={Takayuki Miyazaki and Yasuhiko Minamide},

  journal={Journal of Information Processing},

  volume={27},

  number={ },

  pages={422-430},

  year={2019},

  doi={10.2197/ipsjjip.27.422}

}

%% look-aheads------------------------

%% -------------------------------------

%% back-references--------------------

@article{FERNAU2015287,

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

journal = {Information and Computation},

volume = {242},

pages = {287-305},

year = {2015},

issn = {0890-5401},

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

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

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

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

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.}

}

@inproceedings{Schmid2012,

author = {M.L.~Schmid},

title = {Inside the Class of REGEX Languages},

year = {2012},

isbn = {9783642316524},

publisher = {Springer-Verlag},

address = {Berlin, Heidelberg},

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

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

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.},

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

pages = {73–84},

numpages = {12},

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

location = {Taipei, Taiwan},

series = {DLT'12}

}

@article{BERGLUND2022,

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

journal = {Theoretical Computer Science},

year = {2022},

issn = {0304-3975},

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

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

author = {Martin Berglund and Brink {van der Merwe}},

keywords = {Regular expressions, Backreferences},

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.}

}

@article{FREYDENBERGER20191,

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

journal = {Journal of Computer and System Sciences},

volume = {105},

pages = {1-39},

year = {2019},

issn = {0022-0000},

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

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

author = {Dominik D. Freydenberger and Markus L. Schmid},

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

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.}

}

@InProceedings{Frey2013,

  author =	{Dominik D. Freydenberger},

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

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

  pages =	{507--518},

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

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

  ISSN =	{1868-8969},

  year =	{2011},

  volume =	{9},

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

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

  address =	{Dagstuhl, Germany},

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

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

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

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

}

%% -------------------------- campeanu related

@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},

year = {2009},

month = {05},

pages = {193-207},

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

volume = {46},

journal = {Acta Inf.},

doi = {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 = {Cezar C{\^a}mpeanu and Nicolae 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}}

%% back-references--------------------

%% -------------------------------------

@article{fowler2003,

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

  author={Fowler, Glenn},

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

  year={2003}

}

@inproceedings{Snort1999,

author = {Roesch, Martin},

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

year = {1999},

publisher = {USENIX Association},

address = {USA},

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.},

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

pages = {229–238},

numpages = {10},

location = {Seattle, Washington},

series = {LISA '99}

}

@inproceedings{Becchi08,

author = {Becchi, Michela and Crowley, Patrick},

year = {2008},

month = {01},

pages = {25},

title = {Extending finite automata to efficiently match Perl-compatible regular expressions},

doi = {10.1145/1544012.1544037}

}

@book{

	Sakarovitch2009, 

	place={Cambridge}, 

	title={Elements of Automata Theory}, 

	DOI={10.1017/CBO9781139195218}, 

	publisher={Cambridge University Press}, 

	author={Sakarovitch, Jacques}, 

	editor={Thomas, ReubenTranslator}, 

	year={2009}

}

@unpublished{CSL2022,

author = "Chengsong Tan and Christian Urban",

title = "POSIX Lexing with Bitcoded Derivatives",

note = "submitted",

}

@INPROCEEDINGS{Verbatim,  author={Egolf, Derek and Lasser, Sam and Fisher, Kathleen},  booktitle={2021 IEEE Security and Privacy Workshops (SPW)},   title={Verbatim: A Verified Lexer Generator},   year={2021},  volume={},  number={},  pages={92-100},  doi={10.1109/SPW53761.2021.00022}}

@inproceedings{Verbatimpp,

author = {Egolf, Derek and Lasser, Sam and Fisher, Kathleen},

title = {Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives},

year = {2022},

isbn = {9781450391825},

publisher = {Association for Computing Machinery},

address = {New York, NY, USA},

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

doi = {10.1145/3497775.3503694},

abstract = {Lexers and parsers are attractive targets for attackers because they often sit at the boundary between a software system's internals and the outside world. Formally verified lexers can reduce the attack surface of these systems, thus making them more secure. One recent step in this direction is the development of Verbatim, a verified lexer based on the concept of Brzozowski derivatives. Two limitations restrict the tool's usefulness. First, its running time is quadratic in the length of its input string. Second, the lexer produces tokens with a simple "tag and string" representation, which limits the tool's ability to integrate with parsers that operate on more expressive token representations. In this work, we present a suite of extensions to Verbatim that overcomes these limitations while preserving the tool's original correctness guarantees. The lexer achieves effectively linear performance on a JSON benchmark through a combination of optimizations that, to our knowledge, has not been previously verified. The enhanced version of Verbatim also enables users to augment their lexical specifications with custom semantic actions, and it uses these actions to produce semantically rich tokens---i.e., tokens that carry values with arbitrary, user-defined types. All extensions were implemented and verified with the Coq Proof Assistant.},

booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs},

pages = {27–39},

numpages = {13},

keywords = {Brzozowski derivatives, formal verification, lexical analysis, semantic actions},

location = {Philadelphia, PA, USA},

series = {CPP 2022}

}

@article{Turo_ov__2020,

	author = {Lenka Turo{\v{n}}ov{\'{a}} and Luk{\'{a}}{\v{s}} Hol{\'{\i}}k and Ond{\v{r}}ej Leng{\'{a}}l and Olli Saarikivi and Margus Veanes and Tom{\'{a}}{\v{s}} Vojnar},

	date-added = {2022-05-23 18:43:04 +0100},

	date-modified = {2022-05-23 18:43:04 +0100},

	doi = {10.1145/3428286},

	journal = {Proceedings of the {ACM} on Programming Languages},

	month = {nov},

	number = {{OOPSLA}},

	pages = {1--30},

	publisher = {Association for Computing Machinery ({ACM})},

	title = {Regex matching with counting-set automata},

	url = {https://doi.org/10.1145%2F3428286},

	volume = {4},

	year = 2020,

	bdsk-url-1 = {https://doi.org/10.1145%2F3428286},

	bdsk-url-2 = {https://doi.org/10.1145/3428286}}

@article{Rathnayake2014StaticAF,

	author = {Asiri Rathnayake and Hayo Thielecke},

	journal = {ArXiv},

	title = {Static Analysis for Regular Expression Exponential Runtime via Substructural Logics},

	volume = {abs/1405.7058},

	year = {2014}}

@inproceedings{Weideman2017Static,

	author = {Nicolaas Weideman},

	title = {Static analysis of regular expressions},

	year = {2017}}

@inproceedings{RibeiroAgda2017,

	abstract = {We describe the formalization of a regular expression (RE) parsing algorithm that produces a bit representation of its parse tree in the dependently typed language Agda. The algorithm computes bit-codes using Brzozowski derivatives and we prove that produced codes are equivalent to parse trees ensuring soundness and completeness w.r.t an inductive RE semantics. We include the certified algorithm in a tool developed by us, named verigrep, for regular expression based search in the style of the well known GNU grep. Practical experiments conducted with this tool are reported.},

	address = {New York, NY, USA},

	articleno = {4},

	author = {Ribeiro, Rodrigo and Bois, Andr\'{e} Du},

	booktitle = {Proceedings of the 21st Brazilian Symposium on Programming Languages},

	date-modified = {2022-03-16 16:38:47 +0000},

	doi = {10.1145/3125374.3125381},

	isbn = {9781450353892},

	keywords = {Certified algorithms, regular expressions, dependent types, bit-codes},

	location = {Fortaleza, CE, Brazil},

	numpages = {8},

	publisher = {Association for Computing Machinery},

	series = {SBLP 2017},

	title = {Certified Bit-Coded Regular Expression Parsing},

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

	year = {2017},

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

@article{Thompson_1968,

	author = {Ken Thompson},

	date-added = {2022-02-23 13:44:42 +0000},

	date-modified = {2022-02-23 13:44:42 +0000},

	doi = {10.1145/363347.363387},

	journal = {Communications of the {ACM}},

	month = {jun},

	number = {6},

	pages = {419--422},

	publisher = {Association for Computing Machinery ({ACM})},

	title = {Programming Techniques: Regular expression search algorithm},

	url = {https://doi.org/10.1145%2F363347.363387},

	volume = {11},

	year = 1968,

	bdsk-url-1 = {https://doi.org/10.1145%2F363347.363387},

	bdsk-url-2 = {https://doi.org/10.1145/363347.363387}}

@article{17Bir,

	author = {Asiri Rathnayake and Hayo Thielecke},

	date-added = {2019-08-18 17:57:30 +0000},

	date-modified = {2019-08-18 18:00:13 +0000},

	journal = {arXiv:1405.7058},

	title = {Static Analysis for Regular Expression Exponential Runtime via Substructural Logics},

	year = {2017}}

@article{alfred2014algorithms,

	author = {Alfred, V},

	journal = {Algorithms and Complexity},

	pages = {255},

	publisher = {Elsevier},

	title = {Algorithms for finding patterns in strings},

	volume = {1},

	year = {2014}}

@article{nielson11bcre,

	author = {Lasse Nielsen, Fritz Henglein},

	date-added = {2019-07-03 21:09:39 +0000},

	date-modified = {2019-07-03 21:17:33 +0000},

	journal = {LATA},

	title = {Bit-coded Regular Expression Parsing},

	year = {2011},

	bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxA1Li4vLi4vLi4vTXkgTWFjIChNYWNCb29rLVBybykvRGVza3RvcC9mcml0ei1wYXBlci5wZGZPEQF+AAAAAAF+AAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8PZnJpdHotcGFwZXIucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAMAAAogY3UAAAAAAAAAAAAAAAAAB0Rlc2t0b3AAAAIAQi86VXNlcnM6Y3N0YW46RHJvcGJveDpNeSBNYWMgKE1hY0Jvb2stUHJvKTpEZXNrdG9wOmZyaXR6LXBhcGVyLnBkZgAOACAADwBmAHIAaQB0AHoALQBwAGEAcABlAHIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAEBVc2Vycy9jc3Rhbi9Ecm9wYm94L015IE1hYyAoTWFjQm9vay1Qcm8pL0Rlc2t0b3AvZnJpdHotcGFwZXIucGRmABMAAS8AABUAAgAM//8AAAAIAA0AGgAkAFwAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAAB3g==}}

@software{regexploit2021,

	author = {Ben Caller, Luca Carettoni},

	date-added = {2020-11-24 00:00:00 +0000},

	date-modified = {2021-05-07 00:00:00 +0000},

	keywords = {ReDos static analyser},

	month = {May},

	title = {regexploit},

	url = {https://github.com/doyensec/regexploit},

	year = {2021},

	bdsk-url-1 = {https://github.com/doyensec/regexploit}}