%% 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) 

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

}

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{campeanu2003formal,

	author = {C{\^a}mpeanu, Cezar and Salomaa, Kai and Yu, Sheng},

	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{alfred2014algorithms,

	author = {Alfred, V},

	journal = {Algorithms and Complexity},

	pages = {255},

	publisher = {Elsevier},

	title = {Algorithms for finding patterns in strings},

	volume = {1},

	year = {2014}}

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

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

@misc{KuklewiczHaskell,

	author = {Kuklewicz},

	keywords = {Buggy C POSIX Lexing Libraries},

	title = {Regex Posix},

	url = {https://wiki.haskell.org/Regex_Posix},

	year = {2017},

	bdsk-url-1 = {https://wiki.haskell.org/Regex_Posix}}

@misc{regex101,

	author = {Firas Dib},

	keywords = {regex tester debugger},

	title = {regex101},

	url = {https://regex101.com/},

	year = {2011},

	bdsk-url-1 = {https://regex101.com/}}

@misc{atomEditor,

	author = {Dunno},

	keywords = {text editor},

	title = {Atom Editor},

	url = {https://atom.io},

	year = {2022},

	bdsk-url-1 = {https://atom.io}}

@techreport{grathwohl2014crash,

	author = {Grathwohl, Niels Bj{\o}rn Bugge and Henglein, Fritz and Rasmussen, Ulrik Terp},

	institution = {Technical report, University of Copenhagen},

	title = {A Crash-Course in Regular Expression Parsing and Regular Expressions as Types},

	year = {2014}}

@inproceedings{xml2015,

author = {Bj\"{o}rklund, Henrik and Martens, Wim and Timm, Thomas},

title = {Efficient Incremental Evaluation of Succinct Regular Expressions},

year = {2015},

isbn = {9781450337946},

publisher = {Association for Computing Machinery},

address = {New York, NY, USA},

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

doi = {10.1145/2806416.2806434},

abstract = {Regular expressions are omnipresent in database applications. They form the structural core of schema languages for XML, they are a fundamental ingredient for navigational queries in graph databases, and are being considered in languages for upcoming technologies such as schema- and transformation languages for tabular data on the Web. In this paper we study the usage and effectiveness of the counting operator (or: limited repetition) in regular expressions. The counting operator is a popular extension which is part of the POSIX standard and therefore also present in regular expressions in grep, Java, Python, Perl, and Ruby. In a database context, expressions with counting appear in XML Schema and languages for querying graphs such as SPARQL 1.1 and Cypher.We first present a practical study that suggests that counters are extensively used in practice. We then investigate evaluation methods for such expressions and develop a new algorithm for efficient incremental evaluation. Finally, we conduct an extensive benchmark study that shows that exploiting counting operators can lead to speed-ups of several orders of magnitude in a wide range of settings: normal and incremental evaluation on synthetic and real expressions.},

booktitle = {Proceedings of the 24th ACM International on Conference on Information and Knowledge Management},

pages = {1541–1550},

numpages = {10},

keywords = {regular expressions, schema, regular path queries, xml},

location = {Melbourne, Australia},

series = {CIKM '15}

}

@misc{SE16,

	author = {StackStatus},

	date-added = {2019-06-26 11:28:41 +0000},

	date-modified = {2019-06-26 16:07:31 +0000},

	keywords = {ReDos Attack},

	month = {July},

	rating = {5},

	read = {1},

	title = {Stack Overflow Outage Postmortem},

	url = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016},

	year = {2016},

	bdsk-url-1 = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}}

@article{HosoyaVouillonPierce2005,

	author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce},

	journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},

	number = 1,

	pages = {46--90},

	title = {{R}egular {E}xpression {T}ypes for {XML}},

	volume = 27,

	year = {2005}}

@misc{POSIX,

	note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}},

	title = {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition},

	year = {2004}}

@inproceedings{AusafDyckhoffUrban2016,

	author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},

	booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)},

	pages = {69--86},

	series = {LNCS},

	title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)},

	volume = {9807},

	year = {2016}}

@article{aduAFP16,

	author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},

	issn = {2150-914x},

	journal = {Archive of Formal Proofs},

	note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development},

	title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions},

	year = 2016}

@techreport{CrashCourse2014,

	annote = {draft report},

	author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen},

	institution = {University of Copenhagen},

	title = {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular {E}xpressions as {T}ypes},

	year = {2014}}

@inproceedings{Sulzmann2014,

	author = {M.~Sulzmann and K.~Lu},

	booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)},

	pages = {203--220},

	series = {LNCS},

	title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives},

	volume = {8475},

	year = {2014}}

@inproceedings{Sulzmann2014b,

	author = {M.~Sulzmann and P.~van Steenhoven},

	booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)},

	pages = {174--191},

	series = {LNCS},

	title = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular {E}xpression {S}ubmatching},

	volume = {8409},

	year = {2014}}

@book{Pierce2015,

	author = {B.~C.~Pierce and C.~Casinghino and M.~Gaboardi and M.~Greenberg and C.~Hri\c{t}cu and V.~Sj\"{o}berg and B.~Yorgey},

	note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}},

	publisher = {Electronic textbook},

	title = {{S}oftware {F}oundations},

	year = {2015}}

@misc{Kuklewicz,

	author = {C.~Kuklewicz},

	howpublished = {\url{https://wiki.haskell.org/Regex_Posix}},

	title = {{R}egex {P}osix}}

@article{Vansummeren2006,

	author = {S.~Vansummeren},

	journal = {ACM Transactions on Programming Languages and Systems},

	number = {3},

	pages = {389--428},

	title = {{T}ype {I}nference for {U}nique {P}attern {M}atching},

	volume = {28},

	year = {2006}}

@inproceedings{Asperti12,

	author = {A.~Asperti},

	booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)},

	pages = {283--298},

	series = {LNCS},

	title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},

	volume = {7406},

	year = {2012}}

@inproceedings{Frisch2004,

	author = {A.~Frisch and L.~Cardelli},

	booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)},

	pages = {618--629},

	series = {LNCS},

	title = {{G}reedy {R}egular {E}xpression {M}atching},

	volume = {3142},

	year = {2004}}

@article{Antimirov95,

	author = {V.~Antimirov},

	journal = {Theoretical Computer Science},

	pages = {291--319},

	title = {{P}artial {D}erivatives of {R}egular {E}xpressions and {F}inite {A}utomata {C}onstructions},

	volume = {155},

	year = {1995}}

@inproceedings{Nipkow98,

	author = {T.~Nipkow},

	booktitle = {Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)},

	pages = {1--15},

	series = {LNCS},

	title = {{V}erified {L}exical {A}nalysis},

	volume = 1479,

	year = 1998}

@article{Brzozowski1964,

	author = {J.~A.~Brzozowski},

	journal = {Journal of the {ACM}},

	number = {4},

	pages = {481--494},

	title = {{D}erivatives of {R}egular {E}xpressions},

	volume = {11},

	year = {1964}}

@article{Leroy2009,

	author = {X.~Leroy},

	journal = {Communications of the ACM},

	number = 7,

	pages = {107--115},

	title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler},

	volume = 52,

	year = 2009}

@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{Wu2014,

	author = {C.~Wu and X.~Zhang and C.~Urban},

	journal = {Journal of Automatic Reasoning},

	number = {4},

	pages = {451--480},

	title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},

	volume = {52},

	year = {2014}}

@inproceedings{Regehr2011,

	author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr},

	booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)},

	pages = {283--294},

	title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers},

	year = {2011}}

@article{Norrish2014,

	author = {A.~Barthwal and M.~Norrish},

	journal = {Journal of Computer and System Sciences},

	number = {2},

	pages = {346--362},

	title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}},

	volume = {80},

	year = {2014}}

@article{Thompson1968,

	author = {K.~Thompson},

	issue_date = {June 1968},

	journal = {Communications of the ACM},

	number = {6},

	pages = {419--422},

	title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm},

	volume = {11},

	year = {1968}}

@article{Owens2009,

	author = {S.~Owens and J.~H.~Reppy and A.~Turon},

	journal = {Journal of Functinal Programming},

	number = {2},

	pages = {173--190},

	title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},

	volume = {19},

	year = {2009}}

@inproceedings{Sulzmann2015,

	author = {M.~Sulzmann and P.~Thiemann},

	booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory and Applications (LATA)},

	pages = {275--286},

	series = {LNCS},

	title = {{D}erivatives for {R}egular {S}huffle {E}xpressions},

	volume = {8977},

	year = {2015}}

@inproceedings{Chen2012,

	author = {H.~Chen and S.~Yu},

	booktitle = {Proc.~in the International Workshop on Theoretical Computer Science (WTCS)},

	pages = {343--356},

	series = {LNCS},

	title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication},

	volume = {7160},

	year = {2012}}

@article{Krauss2011,

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

	journal = {Journal of Automated Reasoning},

	pages = {95--106},

	title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},

	volume = 49,

	year = 2012}

@inproceedings{Traytel2015,

	author = {D.~Traytel},

	booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)},

	pages = {487--503},

	series = {LIPIcs},

	title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}},

	volume = {41},

	year = {2015}}

@inproceedings{Traytel2013,

	author = {D.~Traytel and T.~Nipkow},

	booktitle = {Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)},

	pages = {3-12},

	title = {{A} {V}erified {D}ecision {P}rocedure for {MSO} on {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions},

	year = 2013}

@inproceedings{Coquand2012,

	author = {T.~Coquand and V.~Siles},

	booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)},

	pages = {119--134},

	series = {LNCS},

	title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},

	volume = {7086},

	year = {2011}}

@inproceedings{Almeidaetal10,

	author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa},

	booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)},

	pages = {59-68},

	series = {LNCS},

	title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq},

	volume = {6482},

	year = {2010}}