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