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