468
+ − 1
%% This BibTeX bibliography file was created using BibDesk.
+ − 2
%% https://bibdesk.sourceforge.io/
+ − 3
518
+ − 4
%% Created for CS TAN at 2022-05-23 18:43:50 +0100
468
+ − 5
+ − 6
+ − 7
%% Saved with string encoding Unicode (UTF-8)
607
+ − 8
608
+ − 9
+ − 10
+ − 11
+ − 12
%% back-references--------------------
+ − 13
@incollection{AHO1990255,
+ − 14
title = {CHAPTER 5 - Algorithms for Finding Patterns in Strings},
+ − 15
editor = {JAN {VAN LEEUWEN}},
+ − 16
booktitle = {Algorithms and Complexity},
+ − 17
publisher = {Elsevier},
+ − 18
address = {Amsterdam},
+ − 19
pages = {255-300},
+ − 20
year = {1990},
+ − 21
series = {Handbook of Theoretical Computer Science},
+ − 22
isbn = {978-0-444-88071-0},
+ − 23
doi = {https://doi.org/10.1016/B978-0-444-88071-0.50010-2},
+ − 24
url = {https://www.sciencedirect.com/science/article/pii/B9780444880710500102},
+ − 25
author = {Alfred V. AHO},
+ − 26
abstract = {Publisher Summary
+ − 27
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.}
+ − 28
}
+ − 29
+ − 30
%% back-references--------------------
+ − 31
607
+ − 32
@article{fowler2003,
+ − 33
title={An interpretation of the POSIX regex standard},
+ − 34
author={Fowler, Glenn},
+ − 35
journal={URL: https://web. archive. org/web/20050408073627/http://www. research. att. com/\~{} gsf/testregex/re-interpretation. html},
+ − 36
year={2003}
+ − 37
}
+ − 38
+ − 39
+ − 40
@inproceedings{Snort1999,
+ − 41
author = {Roesch, Martin},
+ − 42
title = {Snort - Lightweight Intrusion Detection for Networks},
+ − 43
year = {1999},
+ − 44
publisher = {USENIX Association},
+ − 45
address = {USA},
+ − 46
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.},
+ − 47
booktitle = {Proceedings of the 13th USENIX Conference on System Administration},
+ − 48
pages = {229–238},
+ − 49
numpages = {10},
+ − 50
location = {Seattle, Washington},
+ − 51
series = {LISA '99}
+ − 52
}
+ − 53
606
+ − 54
@inproceedings{Becchi08,
+ − 55
author = {Becchi, Michela and Crowley, Patrick},
+ − 56
year = {2008},
+ − 57
month = {01},
+ − 58
pages = {25},
+ − 59
title = {Extending finite automata to efficiently match Perl-compatible regular expressions},
+ − 60
doi = {10.1145/1544012.1544037}
+ − 61
}
603
+ − 62
605
+ − 63
@book{
+ − 64
Sakarovitch2009,
+ − 65
place={Cambridge},
+ − 66
title={Elements of Automata Theory},
+ − 67
DOI={10.1017/CBO9781139195218},
+ − 68
publisher={Cambridge University Press},
+ − 69
author={Sakarovitch, Jacques},
+ − 70
editor={Thomas, ReubenTranslator},
+ − 71
year={2009}
+ − 72
}
+ − 73
+ − 74
607
+ − 75
@unpublished{CSL2022,
603
+ − 76
author = "Chengsong Tan and Christian Urban",
+ − 77
title = "POSIX Lexing with Bitcoded Derivatives",
+ − 78
note = "submitted",
+ − 79
}
+ − 80
601
+ − 81
@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}}
468
+ − 82
518
+ − 83
601
+ − 84
@inproceedings{Verbatimpp,
+ − 85
author = {Egolf, Derek and Lasser, Sam and Fisher, Kathleen},
+ − 86
title = {Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives},
+ − 87
year = {2022},
+ − 88
isbn = {9781450391825},
+ − 89
publisher = {Association for Computing Machinery},
+ − 90
address = {New York, NY, USA},
+ − 91
url = {https://doi.org/10.1145/3497775.3503694},
+ − 92
doi = {10.1145/3497775.3503694},
+ − 93
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.},
+ − 94
booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+ − 95
pages = {27–39},
+ − 96
numpages = {13},
+ − 97
keywords = {Brzozowski derivatives, formal verification, lexical analysis, semantic actions},
+ − 98
location = {Philadelphia, PA, USA},
+ − 99
series = {CPP 2022}
+ − 100
}
+ − 101
518
+ − 102
+ − 103
@article{Turo_ov__2020,
+ − 104
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},
+ − 105
date-added = {2022-05-23 18:43:04 +0100},
+ − 106
date-modified = {2022-05-23 18:43:04 +0100},
+ − 107
doi = {10.1145/3428286},
+ − 108
journal = {Proceedings of the {ACM} on Programming Languages},
+ − 109
month = {nov},
+ − 110
number = {{OOPSLA}},
+ − 111
pages = {1--30},
+ − 112
publisher = {Association for Computing Machinery ({ACM})},
+ − 113
title = {Regex matching with counting-set automata},
+ − 114
url = {https://doi.org/10.1145%2F3428286},
+ − 115
volume = {4},
+ − 116
year = 2020,
+ − 117
bdsk-url-1 = {https://doi.org/10.1145%2F3428286},
+ − 118
bdsk-url-2 = {https://doi.org/10.1145/3428286}}
+ − 119
468
+ − 120
@article{Rathnayake2014StaticAF,
518
+ − 121
author = {Asiri Rathnayake and Hayo Thielecke},
+ − 122
journal = {ArXiv},
+ − 123
title = {Static Analysis for Regular Expression Exponential Runtime via Substructural Logics},
+ − 124
volume = {abs/1405.7058},
+ − 125
year = {2014}}
468
+ − 126
472
+ − 127
@inproceedings{Weideman2017Static,
518
+ − 128
author = {Nicolaas Weideman},
+ − 129
title = {Static analysis of regular expressions},
+ − 130
year = {2017}}
472
+ − 131
468
+ − 132
@inproceedings{RibeiroAgda2017,
+ − 133
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.},
+ − 134
address = {New York, NY, USA},
+ − 135
articleno = {4},
+ − 136
author = {Ribeiro, Rodrigo and Bois, Andr\'{e} Du},
+ − 137
booktitle = {Proceedings of the 21st Brazilian Symposium on Programming Languages},
+ − 138
date-modified = {2022-03-16 16:38:47 +0000},
+ − 139
doi = {10.1145/3125374.3125381},
+ − 140
isbn = {9781450353892},
+ − 141
keywords = {Certified algorithms, regular expressions, dependent types, bit-codes},
+ − 142
location = {Fortaleza, CE, Brazil},
+ − 143
numpages = {8},
+ − 144
publisher = {Association for Computing Machinery},
+ − 145
series = {SBLP 2017},
+ − 146
title = {Certified Bit-Coded Regular Expression Parsing},
+ − 147
url = {https://doi.org/10.1145/3125374.3125381},
+ − 148
year = {2017},
+ − 149
bdsk-url-1 = {https://doi.org/10.1145/3125374.3125381}}
+ − 150
+ − 151
@article{Thompson_1968,
+ − 152
author = {Ken Thompson},
+ − 153
date-added = {2022-02-23 13:44:42 +0000},
+ − 154
date-modified = {2022-02-23 13:44:42 +0000},
+ − 155
doi = {10.1145/363347.363387},
+ − 156
journal = {Communications of the {ACM}},
+ − 157
month = {jun},
+ − 158
number = {6},
+ − 159
pages = {419--422},
+ − 160
publisher = {Association for Computing Machinery ({ACM})},
+ − 161
title = {Programming Techniques: Regular expression search algorithm},
+ − 162
url = {https://doi.org/10.1145%2F363347.363387},
+ − 163
volume = {11},
+ − 164
year = 1968,
+ − 165
bdsk-url-1 = {https://doi.org/10.1145%2F363347.363387},
+ − 166
bdsk-url-2 = {https://doi.org/10.1145/363347.363387}}
+ − 167
+ − 168
@article{17Bir,
+ − 169
author = {Asiri Rathnayake and Hayo Thielecke},
+ − 170
date-added = {2019-08-18 17:57:30 +0000},
+ − 171
date-modified = {2019-08-18 18:00:13 +0000},
+ − 172
journal = {arXiv:1405.7058},
+ − 173
title = {Static Analysis for Regular Expression Exponential Runtime via Substructural Logics},
+ − 174
year = {2017}}
518
+ − 175
471
+ − 176
@article{campeanu2003formal,
518
+ − 177
author = {C{\^a}mpeanu, Cezar and Salomaa, Kai and Yu, Sheng},
+ − 178
journal = {International Journal of Foundations of Computer Science},
+ − 179
number = {06},
+ − 180
pages = {1007--1018},
+ − 181
publisher = {World Scientific},
+ − 182
title = {A formal study of practical regular expressions},
+ − 183
volume = {14},
+ − 184
year = {2003}}
471
+ − 185
+ − 186
@article{alfred2014algorithms,
518
+ − 187
author = {Alfred, V},
+ − 188
journal = {Algorithms and Complexity},
+ − 189
pages = {255},
+ − 190
publisher = {Elsevier},
+ − 191
title = {Algorithms for finding patterns in strings},
+ − 192
volume = {1},
+ − 193
year = {2014}}
471
+ − 194
+ − 195
@article{CAMPEANU2009Intersect,
518
+ − 196
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.},
+ − 197
author = {Cezar C{\^a}mpeanu and Nicolae Santean},
+ − 198
doi = {https://doi.org/10.1016/j.tcs.2009.02.022},
+ − 199
issn = {0304-3975},
+ − 200
journal = {Theoretical Computer Science},
+ − 201
keywords = {Extended regular expression, Regex automata system, Regex},
+ − 202
note = {Formal Languages and Applications: A Collection of Papers in Honor of Sheng Yu},
+ − 203
number = {24},
+ − 204
pages = {2336-2344},
+ − 205
title = {On the intersection of regex languages with regular languages},
+ − 206
url = {https://www.sciencedirect.com/science/article/pii/S0304397509001789},
+ − 207
volume = {410},
+ − 208
year = {2009},
+ − 209
bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397509001789},
+ − 210
bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2009.02.022}}
468
+ − 211
+ − 212
@article{nielson11bcre,
+ − 213
author = {Lasse Nielsen, Fritz Henglein},
+ − 214
date-added = {2019-07-03 21:09:39 +0000},
+ − 215
date-modified = {2019-07-03 21:17:33 +0000},
+ − 216
journal = {LATA},
+ − 217
title = {Bit-coded Regular Expression Parsing},
+ − 218
year = {2011},
+ − 219
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxA1Li4vLi4vLi4vTXkgTWFjIChNYWNCb29rLVBybykvRGVza3RvcC9mcml0ei1wYXBlci5wZGZPEQF+AAAAAAF+AAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8PZnJpdHotcGFwZXIucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAMAAAogY3UAAAAAAAAAAAAAAAAAB0Rlc2t0b3AAAAIAQi86VXNlcnM6Y3N0YW46RHJvcGJveDpNeSBNYWMgKE1hY0Jvb2stUHJvKTpEZXNrdG9wOmZyaXR6LXBhcGVyLnBkZgAOACAADwBmAHIAaQB0AHoALQBwAGEAcABlAHIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAEBVc2Vycy9jc3Rhbi9Ecm9wYm94L015IE1hYyAoTWFjQm9vay1Qcm8pL0Rlc2t0b3AvZnJpdHotcGFwZXIucGRmABMAAS8AABUAAgAM//8AAAAIAA0AGgAkAFwAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAAB3g==}}
518
+ − 220
468
+ − 221
@software{regexploit2021,
+ − 222
author = {Ben Caller, Luca Carettoni},
+ − 223
date-added = {2020-11-24 00:00:00 +0000},
+ − 224
date-modified = {2021-05-07 00:00:00 +0000},
+ − 225
keywords = {ReDos static analyser},
472
+ − 226
month = {May},
+ − 227
title = {regexploit},
+ − 228
url = {https://github.com/doyensec/regexploit},
518
+ − 229
year = {2021},
+ − 230
bdsk-url-1 = {https://github.com/doyensec/regexploit}}
+ − 231
608
+ − 232
@software{pcre,
+ − 233
author = {Philip Hazel},
+ − 234
date-added = {1997-01-01 00:00:00 +0000},
+ − 235
date-modified = {2021-06-14 00:00:00 +0000},
+ − 236
keywords = {Perl Compatible Regular Expressions},
+ − 237
month = {June},
+ − 238
title = {PCRE},
+ − 239
url = {https://www.pcre.org/original/doc/html/},
+ − 240
year = {2021},
+ − 241
bdsk-url-1 = {https://www.pcre.org/original/doc/html/}
+ − 242
}
+ − 243
471
+ − 244
@misc{KuklewiczHaskell,
+ − 245
author = {Kuklewicz},
+ − 246
keywords = {Buggy C POSIX Lexing Libraries},
518
+ − 247
title = {Regex Posix},
471
+ − 248
url = {https://wiki.haskell.org/Regex_Posix},
518
+ − 249
year = {2017},
+ − 250
bdsk-url-1 = {https://wiki.haskell.org/Regex_Posix}}
+ − 251
472
+ − 252
@misc{regex101,
+ − 253
author = {Firas Dib},
518
+ − 254
keywords = {regex tester debugger},
+ − 255
title = {regex101},
472
+ − 256
url = {https://regex101.com/},
518
+ − 257
year = {2011},
+ − 258
bdsk-url-1 = {https://regex101.com/}}
+ − 259
500
+ − 260
@misc{atomEditor,
518
+ − 261
author = {Dunno},
+ − 262
keywords = {text editor},
500
+ − 263
title = {Atom Editor},
518
+ − 264
url = {https://atom.io},
500
+ − 265
year = {2022},
518
+ − 266
bdsk-url-1 = {https://atom.io}}
+ − 267
471
+ − 268
@techreport{grathwohl2014crash,
518
+ − 269
author = {Grathwohl, Niels Bj{\o}rn Bugge and Henglein, Fritz and Rasmussen, Ulrik Terp},
+ − 270
institution = {Technical report, University of Copenhagen},
+ − 271
title = {A Crash-Course in Regular Expression Parsing and Regular Expressions as Types},
+ − 272
year = {2014}}
471
+ − 273
602
+ − 274
@inproceedings{xml2015,
+ − 275
author = {Bj\"{o}rklund, Henrik and Martens, Wim and Timm, Thomas},
+ − 276
title = {Efficient Incremental Evaluation of Succinct Regular Expressions},
+ − 277
year = {2015},
+ − 278
isbn = {9781450337946},
+ − 279
publisher = {Association for Computing Machinery},
+ − 280
address = {New York, NY, USA},
+ − 281
url = {https://doi.org/10.1145/2806416.2806434},
+ − 282
doi = {10.1145/2806416.2806434},
+ − 283
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.},
+ − 284
booktitle = {Proceedings of the 24th ACM International on Conference on Information and Knowledge Management},
+ − 285
pages = {1541–1550},
+ − 286
numpages = {10},
+ − 287
keywords = {regular expressions, schema, regular path queries, xml},
+ − 288
location = {Melbourne, Australia},
+ − 289
series = {CIKM '15}
+ − 290
}
+ − 291
+ − 292
468
+ − 293
@misc{SE16,
+ − 294
author = {StackStatus},
+ − 295
date-added = {2019-06-26 11:28:41 +0000},
+ − 296
date-modified = {2019-06-26 16:07:31 +0000},
+ − 297
keywords = {ReDos Attack},
+ − 298
month = {July},
+ − 299
rating = {5},
+ − 300
read = {1},
+ − 301
title = {Stack Overflow Outage Postmortem},
+ − 302
url = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016},
+ − 303
year = {2016},
+ − 304
bdsk-url-1 = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}}
+ − 305
+ − 306
@article{HosoyaVouillonPierce2005,
+ − 307
author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce},
+ − 308
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
+ − 309
number = 1,
+ − 310
pages = {46--90},
+ − 311
title = {{R}egular {E}xpression {T}ypes for {XML}},
+ − 312
volume = 27,
+ − 313
year = {2005}}
+ − 314
+ − 315
@misc{POSIX,
+ − 316
note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}},
+ − 317
title = {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition},
+ − 318
year = {2004}}
+ − 319
+ − 320
@inproceedings{AusafDyckhoffUrban2016,
+ − 321
author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},
+ − 322
booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)},
+ − 323
pages = {69--86},
+ − 324
series = {LNCS},
+ − 325
title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)},
+ − 326
volume = {9807},
+ − 327
year = {2016}}
+ − 328
+ − 329
@article{aduAFP16,
+ − 330
author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},
+ − 331
issn = {2150-914x},
+ − 332
journal = {Archive of Formal Proofs},
+ − 333
note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development},
+ − 334
title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions},
+ − 335
year = 2016}
+ − 336
+ − 337
@techreport{CrashCourse2014,
+ − 338
annote = {draft report},
+ − 339
author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen},
+ − 340
institution = {University of Copenhagen},
+ − 341
title = {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular {E}xpressions as {T}ypes},
+ − 342
year = {2014}}
+ − 343
+ − 344
@inproceedings{Sulzmann2014,
+ − 345
author = {M.~Sulzmann and K.~Lu},
+ − 346
booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)},
+ − 347
pages = {203--220},
+ − 348
series = {LNCS},
+ − 349
title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives},
+ − 350
volume = {8475},
+ − 351
year = {2014}}
+ − 352
+ − 353
@inproceedings{Sulzmann2014b,
+ − 354
author = {M.~Sulzmann and P.~van Steenhoven},
+ − 355
booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)},
+ − 356
pages = {174--191},
+ − 357
series = {LNCS},
+ − 358
title = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular {E}xpression {S}ubmatching},
+ − 359
volume = {8409},
+ − 360
year = {2014}}
+ − 361
+ − 362
@book{Pierce2015,
+ − 363
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},
+ − 364
note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}},
+ − 365
publisher = {Electronic textbook},
+ − 366
title = {{S}oftware {F}oundations},
+ − 367
year = {2015}}
+ − 368
+ − 369
@misc{Kuklewicz,
+ − 370
author = {C.~Kuklewicz},
+ − 371
howpublished = {\url{https://wiki.haskell.org/Regex_Posix}},
+ − 372
title = {{R}egex {P}osix}}
+ − 373
+ − 374
@article{Vansummeren2006,
+ − 375
author = {S.~Vansummeren},
+ − 376
journal = {ACM Transactions on Programming Languages and Systems},
+ − 377
number = {3},
+ − 378
pages = {389--428},
+ − 379
title = {{T}ype {I}nference for {U}nique {P}attern {M}atching},
+ − 380
volume = {28},
+ − 381
year = {2006}}
+ − 382
+ − 383
@inproceedings{Asperti12,
+ − 384
author = {A.~Asperti},
+ − 385
booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)},
+ − 386
pages = {283--298},
+ − 387
series = {LNCS},
+ − 388
title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},
+ − 389
volume = {7406},
+ − 390
year = {2012}}
+ − 391
+ − 392
@inproceedings{Frisch2004,
+ − 393
author = {A.~Frisch and L.~Cardelli},
+ − 394
booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)},
+ − 395
pages = {618--629},
+ − 396
series = {LNCS},
+ − 397
title = {{G}reedy {R}egular {E}xpression {M}atching},
+ − 398
volume = {3142},
+ − 399
year = {2004}}
+ − 400
+ − 401
@article{Antimirov95,
+ − 402
author = {V.~Antimirov},
+ − 403
journal = {Theoretical Computer Science},
+ − 404
pages = {291--319},
+ − 405
title = {{P}artial {D}erivatives of {R}egular {E}xpressions and {F}inite {A}utomata {C}onstructions},
+ − 406
volume = {155},
+ − 407
year = {1995}}
+ − 408
+ − 409
@inproceedings{Nipkow98,
+ − 410
author = {T.~Nipkow},
+ − 411
booktitle = {Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)},
+ − 412
pages = {1--15},
+ − 413
series = {LNCS},
+ − 414
title = {{V}erified {L}exical {A}nalysis},
+ − 415
volume = 1479,
+ − 416
year = 1998}
+ − 417
+ − 418
@article{Brzozowski1964,
+ − 419
author = {J.~A.~Brzozowski},
+ − 420
journal = {Journal of the {ACM}},
+ − 421
number = {4},
+ − 422
pages = {481--494},
+ − 423
title = {{D}erivatives of {R}egular {E}xpressions},
+ − 424
volume = {11},
+ − 425
year = {1964}}
+ − 426
+ − 427
@article{Leroy2009,
+ − 428
author = {X.~Leroy},
+ − 429
journal = {Communications of the ACM},
+ − 430
number = 7,
+ − 431
pages = {107--115},
+ − 432
title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler},
+ − 433
volume = 52,
+ − 434
year = 2009}
+ − 435
+ − 436
@inproceedings{Paulson2015,
+ − 437
author = {L.~C.~Paulson},
+ − 438
booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)},
+ − 439
pages = {231--245},
+ − 440
series = {LNAI},
+ − 441
title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets},
+ − 442
volume = {9195},
+ − 443
year = {2015}}
+ − 444
+ − 445
@article{Wu2014,
+ − 446
author = {C.~Wu and X.~Zhang and C.~Urban},
+ − 447
journal = {Journal of Automatic Reasoning},
+ − 448
number = {4},
+ − 449
pages = {451--480},
+ − 450
title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},
+ − 451
volume = {52},
+ − 452
year = {2014}}
+ − 453
+ − 454
@inproceedings{Regehr2011,
+ − 455
author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr},
+ − 456
booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)},
+ − 457
pages = {283--294},
+ − 458
title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers},
+ − 459
year = {2011}}
+ − 460
+ − 461
@article{Norrish2014,
+ − 462
author = {A.~Barthwal and M.~Norrish},
+ − 463
journal = {Journal of Computer and System Sciences},
+ − 464
number = {2},
+ − 465
pages = {346--362},
+ − 466
title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}},
+ − 467
volume = {80},
+ − 468
year = {2014}}
+ − 469
+ − 470
@article{Thompson1968,
+ − 471
author = {K.~Thompson},
+ − 472
issue_date = {June 1968},
+ − 473
journal = {Communications of the ACM},
+ − 474
number = {6},
+ − 475
pages = {419--422},
+ − 476
title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm},
+ − 477
volume = {11},
+ − 478
year = {1968}}
+ − 479
+ − 480
@article{Owens2009,
+ − 481
author = {S.~Owens and J.~H.~Reppy and A.~Turon},
+ − 482
journal = {Journal of Functinal Programming},
+ − 483
number = {2},
+ − 484
pages = {173--190},
+ − 485
title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},
+ − 486
volume = {19},
+ − 487
year = {2009}}
+ − 488
+ − 489
@inproceedings{Sulzmann2015,
+ − 490
author = {M.~Sulzmann and P.~Thiemann},
+ − 491
booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory and Applications (LATA)},
+ − 492
pages = {275--286},
+ − 493
series = {LNCS},
+ − 494
title = {{D}erivatives for {R}egular {S}huffle {E}xpressions},
+ − 495
volume = {8977},
+ − 496
year = {2015}}
+ − 497
+ − 498
@inproceedings{Chen2012,
+ − 499
author = {H.~Chen and S.~Yu},
+ − 500
booktitle = {Proc.~in the International Workshop on Theoretical Computer Science (WTCS)},
+ − 501
pages = {343--356},
+ − 502
series = {LNCS},
+ − 503
title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication},
+ − 504
volume = {7160},
+ − 505
year = {2012}}
+ − 506
+ − 507
@article{Krauss2011,
+ − 508
author = {A.~Krauss and T.~Nipkow},
+ − 509
journal = {Journal of Automated Reasoning},
+ − 510
pages = {95--106},
+ − 511
title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
+ − 512
volume = 49,
+ − 513
year = 2012}
+ − 514
+ − 515
@inproceedings{Traytel2015,
+ − 516
author = {D.~Traytel},
+ − 517
booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)},
+ − 518
pages = {487--503},
+ − 519
series = {LIPIcs},
+ − 520
title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}},
+ − 521
volume = {41},
+ − 522
year = {2015}}
+ − 523
+ − 524
@inproceedings{Traytel2013,
+ − 525
author = {D.~Traytel and T.~Nipkow},
+ − 526
booktitle = {Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)},
+ − 527
pages = {3-12},
+ − 528
title = {{A} {V}erified {D}ecision {P}rocedure for {MSO} on {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions},
+ − 529
year = 2013}
+ − 530
+ − 531
@inproceedings{Coquand2012,
+ − 532
author = {T.~Coquand and V.~Siles},
+ − 533
booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)},
+ − 534
pages = {119--134},
+ − 535
series = {LNCS},
+ − 536
title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},
+ − 537
volume = {7086},
+ − 538
year = {2011}}
+ − 539
+ − 540
@inproceedings{Almeidaetal10,
+ − 541
author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa},
+ − 542
booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)},
+ − 543
pages = {59-68},
+ − 544
series = {LNCS},
+ − 545
title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq},
+ − 546
volume = {6482},
+ − 547
year = {2010}}
+ − 548
+ − 549
@article{Owens2008,
+ − 550
author = {S.~Owens and K.~Slind},
+ − 551
journal = {Higher-Order and Symbolic Computation},
+ − 552
number = {4},
+ − 553
pages = {377--409},
+ − 554
title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},
+ − 555
volume = {21},
+ − 556
year = {2008}}
+ − 557
+ − 558
@article{Owens2,
+ − 559
author = {S.~Owens and K.~Slind},
+ − 560
bibsource = {dblp computer science bibliography, http://dblp.org},
+ − 561
biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08},
+ − 562
doi = {10.1007/s10990-008-9038-0},
+ − 563
journal = {Higher-Order and Symbolic Computation},
+ − 564
number = {4},
+ − 565
pages = {377--409},
+ − 566
timestamp = {Wed, 16 Dec 2009 13:51:02 +0100},
+ − 567
title = {Adapting functional programs to higher order logic},
+ − 568
url = {http://dx.doi.org/10.1007/s10990-008-9038-0},
+ − 569
volume = {21},
+ − 570
year = {2008},
+ − 571
bdsk-url-1 = {http://dx.doi.org/10.1007/s10990-008-9038-0}}
+ − 572
+ − 573
@misc{PCRE,
+ − 574
title = {{PCRE - Perl Compatible Regular Expressions}},
+ − 575
url = {http://www.pcre.org},
+ − 576
bdsk-url-1 = {http://www.pcre.org}}
+ − 577
+ − 578
@inproceedings{OkuiSuzuki2010,
+ − 579
author = {S.~Okui and T.~Suzuki},
+ − 580
booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)},
+ − 581
pages = {231--240},
+ − 582
series = {LNCS},
+ − 583
title = {{D}isambiguation in {R}egular {E}xpression {M}atching via {P}osition {A}utomata with {A}ugmented {T}ransitions},
+ − 584
volume = {6482},
+ − 585
year = {2010}}
+ − 586
+ − 587
@techreport{OkuiSuzukiTech,
+ − 588
author = {S.~Okui and T.~Suzuki},
+ − 589
institution = {University of Aizu},
+ − 590
title = {{D}isambiguation in {R}egular {E}xpression {M}atching via {P}osition {A}utomata with {A}ugmented {T}ransitions},
+ − 591
year = {2013}}
+ − 592
+ − 593
@inproceedings{Davis18,
+ − 594
author = {J.~C.~Davis and C.~.A.~Coghlan and F.~Servant and D.~Lee},
+ − 595
booktitle = {Proc.~of the 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)},
+ − 596
numpages = {11},
+ − 597
pages = {246--256},
+ − 598
title = {{T}he {I}mpact of {R}egular {E}xpression {D}enial of {S}ervice ({ReDoS}) in {P}ractice: {A}n {E}mpirical {S}tudy at the {E}cosystem {S}cale},
+ − 599
year = {2018}}