ChengsongTanPhdThesis/example.bib
author Chengsong
Tue, 22 Nov 2022 12:50:04 +0000
changeset 627 94db2636a296
parent 626 1c8525061545
child 628 7af4e2420a8c
permissions -rwxr-xr-x
finished!
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
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
     4
%% Created for CS TAN at 2022-11-20 17:26:32 +0000 
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) 
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
     8
@inproceedings{Doczkal2013,
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
     9
author = {C.~Doczkaland J.O.~Kaiser and G.~Smolka},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    10
title = {A Constructive Theory of Regular Languages in Coq},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    11
year = {2013},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    12
isbn = {9783319035444},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    13
publisher = {Springer-Verlag},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    14
address = {Berlin, Heidelberg},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    15
url = {https://doi.org/10.1007/978-3-319-03545-1_6},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    16
doi = {10.1007/978-3-319-03545-1_6},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    17
abstract = {We present a formal constructive theory of regular languages consisting of about 1400 lines of Coq/Ssreflect. As representations we consider regular expressions, deterministic and nondeterministic automata, and Myhill and Nerode partitions. We construct computable functions translating between these representations and show that equivalence of representations is decidable. We also establish the usual closure properties, give a minimization algorithm for DFAs, and prove that minimal DFAs are unique up to state renaming. Our development profits much from Ssreflect's support for finite types and graphs.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    18
booktitle = {Proceedings of the Third International Conference on Certified Programs and Proofs - Volume 8307},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    19
pages = {82–97},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    20
numpages = {16},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    21
keywords = {finite automata, regular expressions, Myhill-Nerode, Ssreflect, Coq, regular languages}
609
61139fdddae0 chap1 totally done
Chengsong
parents: 608
diff changeset
    22
}
61139fdddae0 chap1 totally done
Chengsong
parents: 608
diff changeset
    23
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    24
@inproceedings{Lammich2012,
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    25
author = {P.~Lammichand T.~Tuerk},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    26
year = {2012},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    27
month = {08},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    28
pages = {166-182},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    29
title = {Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    30
isbn = {978-3-642-32346-1},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    31
doi = {10.1007/978-3-642-32347-8_12}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    32
}
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    33
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    34
@article{Krauss2012,
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    35
	author={A.~Krauss and T.~Nipkow},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    36
title={Proof Pearl: Regular Expression Equivalence and Relation Algebra},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    37
journal={J. Automated Reasoning},volume=49,pages={95--106},year=2012,note={published online March 2011}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    38
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    39
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    40
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    41
@article{kleene1956,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    42
  title={Representation of events in nerve nets and finite automata},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    43
  author={S.C.~Kleene and others},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    44
  journal={Automata studies},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    45
  volume={34},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    46
  pages={3--41},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    47
  year={1956},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    48
  publisher={Princeton, NJ}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    49
}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    50
609
61139fdddae0 chap1 totally done
Chengsong
parents: 608
diff changeset
    51
61139fdddae0 chap1 totally done
Chengsong
parents: 608
diff changeset
    52
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    53
@article{Murugesan2014,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    54
	author = {N.~Murugesan and O.~V.~Shanmuga Sundaram},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    55
	journal = {International Journal of Computer Trends and Technology},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    56
	number = {1},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    57
	pages = {29--33},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    58
	title = {{S}ome {P}roperties of {B}rzozowski {D}erivatives of {R}egular {E}xpressions},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    59
	url = {http://arxiv.org/abs/1407.5902},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    60
	volume = {13},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    61
	year = {2014},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    62
	bdsk-url-1 = {http://arxiv.org/abs/1407.5902}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    63
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    64
@phdthesis{Ausaf,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    65
	author = {F.~Ausaf},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    66
	school = {King's College London},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    67
	title = {{V}erified {L}exing and {P}arsing},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    68
	year = {2018}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    69
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    70
@inproceedings{Okui10,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    71
	abstract = {This paper offers a new efficient regular expression matching algorithm which follows the POSIX-type leftmost-longest rule. The algorithm basically emulates the subset construction without backtracking, so that its computational cost even in the worst case does not explode exponentially; the time complexity of the algorithm is O(mn(n{\thinspace}+{\thinspace}c)), where m is the length of a given input string, n the number of occurrences of the most frequently used letter in a given regular expression and c the number of subexpressions to be used for capturing substrings. A formalization of the leftmost-longest semantics by using parse trees is also discussed.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    72
	address = {Berlin, Heidelberg},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    73
	author = {S.~Okui and T.~Suzuki},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    74
	booktitle = {Implementation and Application of Automata},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    75
	editor = {Domaratzki, Michael and Salomaa, Kai},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    76
	isbn = {978-3-642-18098-9},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    77
	pages = {231--240},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    78
	publisher = {Springer Berlin Heidelberg},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    79
	title = {Disambiguation in Regular Expression Matching via Position Automata with Augmented Transitions},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    80
	year = {2011}}
609
61139fdddae0 chap1 totally done
Chengsong
parents: 608
diff changeset
    81
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    82
@article{Berglund14,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    83
	author = {M.~Berglund, F.~Drewes and B.~Van Der Merwe},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    84
	doi = {10.4204/EPTCS.151.7},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    85
	journal = {Electronic Proceedings in Theoretical Computer Science},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    86
	month = {05},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    87
	title = {Analyzing Catastrophic Backtracking Behavior in Practical Regular Expression Matching},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    88
	volume = {151},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    89
	year = {2014},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    90
	bdsk-url-1 = {https://doi.org/10.4204/EPTCS.151.7}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    91
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    92
@inproceedings{Berglund18,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    93
	abstract = {Whereas Perl-compatible regular expression matchers typically exhibit some variation of leftmost-greedy semantics, those conforming to the posix standard are prescribed leftmost-longest semantics. However, the posix standard leaves some room for interpretation, and Fowler and Kuklewicz have done experimental work to confirm differences between various posix matchers. The Boost library has an interesting take on the posix standard, where it maximises the leftmost match not with respect to subexpressions of the regular expression pattern, but rather, with respect to capturing groups. In our work, we provide the first formalisation of Boost semantics, and we analyse the complexity of regular expression matching when using Boost semantics.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    94
	address = {Cham},
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
    95
	author = {M.~Berglund and W.~Bester and van der M.~Brink},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    96
	booktitle = {Theoretical Aspects of Computing -- ICTAC 2018},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    97
	editor = {Fischer, Bernd and Uustalu, Tarmo},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    98
	isbn = {978-3-030-02508-3},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
    99
	pages = {99--115},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   100
	publisher = {Springer International Publishing},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   101
	title = {Formalising Boost POSIX Regular Expression Matching},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   102
	year = {2018}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   103
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   104
@inproceedings{Chen12,
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   105
	author = {H.~Chenand S.~Yu},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   106
	doi = {10.1007/978-3-642-27654-5_27},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   107
	month = {01},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   108
	pages = {343-356},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   109
	title = {Derivatives of Regular Expressions and an Application},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   110
	volume = {7160},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   111
	year = {2012},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   112
	bdsk-url-1 = {https://doi.org/10.1007/978-3-642-27654-5_27}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   113
609
61139fdddae0 chap1 totally done
Chengsong
parents: 608
diff changeset
   114
@article{Takayuki2019,
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   115
	author = {T.~Miyazaki and Y.~Minamide},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   116
	doi = {10.2197/ipsjjip.27.422},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   117
	journal = {Journal of Information Processing},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   118
	pages = {422-430},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   119
	title = {Derivatives of Regular Expressions with Lookahead},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   120
	volume = {27},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   121
	year = {2019},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   122
	bdsk-url-1 = {https://doi.org/10.2197/ipsjjip.27.422}}
608
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   123
624
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   124
@article{FERNAU2015287,
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   125
	abstract = {A pattern α, i.e., a string that contains variables and terminals, matches a terminal word w if w can be obtained by uniformly substituting the variables of α by terminal words. Deciding whether a given terminal word matches a given pattern is NP-complete and this holds for several natural variants of the problem that result from whether or not variables can be erased, whether or not the patterns are required to be terminal-free or whether or not the mapping of variables to terminal words must be injective. We consider numerous parameters of this problem (i.e., number of variables, length of w, length of the words substituted for variables, number of occurrences per variable, cardinality of the terminal alphabet) and for all possible combinations of the parameters (and variants described above), we answer the question whether or not the problem is still NP-complete if these parameters are bounded by constants.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   126
	author = {H.~Fernau and M.L.~Schmid},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   127
	doi = {https://doi.org/10.1016/j.ic.2015.03.006},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   128
	issn = {0890-5401},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   129
	journal = {Information and Computation},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   130
	keywords = {Parameterised pattern matching, Function matching, NP-completeness, Membership problem for pattern languages, Morphisms},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   131
	pages = {287-305},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   132
	title = {Pattern matching with variables: A multivariate complexity analysis},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   133
	url = {https://www.sciencedirect.com/science/article/pii/S0890540115000218},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   134
	volume = {242},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   135
	year = {2015},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   136
	bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0890540115000218},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   137
	bdsk-url-2 = {https://doi.org/10.1016/j.ic.2015.03.006}}
624
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   138
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   139
@inproceedings{Schmid2012,
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   140
	abstract = {We study different possibilities of combining the concept of homomorphic replacement with regular expressions in order to investigate the class of languages given by extended regular expressions with backreferences (REGEX). It is shown in which regard existing and natural ways to do this fail to reach the expressive power of REGEX. Furthermore, the complexity of the membership problem for REGEX with a bounded number of backreferences is considered.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   141
	address = {Berlin, Heidelberg},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   142
	author = {M.L.~Schmid},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   143
	booktitle = {Proceedings of the 16th International Conference on Developments in Language Theory},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   144
	doi = {10.1007/978-3-642-31653-1_8},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   145
	isbn = {9783642316524},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   146
	keywords = {extended regular expressions, pattern languages, REGEX, pattern expressions, homomorphic replacement},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   147
	location = {Taipei, Taiwan},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   148
	numpages = {12},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   149
	pages = {73--84},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   150
	publisher = {Springer-Verlag},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   151
	series = {DLT'12},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   152
	title = {Inside the Class of REGEX Languages},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   153
	url = {https://doi.org/10.1007/978-3-642-31653-1_8},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   154
	year = {2012},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   155
	bdsk-url-1 = {https://doi.org/10.1007/978-3-642-31653-1_8}}
624
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   156
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   157
@article{BERGLUND2022,
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   158
	abstract = {Most modern regular expression matching libraries (one of the rare exceptions being Google's RE2) allow backreferences, operations which bind a substring to a variable, allowing it to be matched again verbatim. However, both real-world implementations and definitions in the literature use different syntactic restrictions and have differences in the semantics of the matching of backreferences. Our aim is to compare these various flavors by considering the classes of formal languages that each can describe, establishing, as a result, a hierarchy of language classes. Beyond the hierarchy itself, some complexity results are given, and as part of the effort on comparing language classes new pumping lemmas are established, old classes are extended to new ones, and several incidental results on the nature of these language classes are given.},
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   159
	author = {M.~Berglund and van der M.~Brink },
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   160
	doi = {https://doi.org/10.1016/j.tcs.2022.10.041},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   161
	issn = {0304-3975},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   162
	journal = {Theoretical Computer Science},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   163
	keywords = {Regular expressions, Backreferences},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   164
	title = {Re-examining regular expressions with backreferences},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   165
	url = {https://www.sciencedirect.com/science/article/pii/S0304397522006570},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   166
	year = {2022},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   167
	bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397522006570},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   168
	bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2022.10.041}}
608
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   169
624
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   170
@article{FREYDENBERGER20191,
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   171
	abstract = {Most modern libraries for regular expression matching allow back-references (i.e., repetition operators) that substantially increase expressive power, but also lead to intractability. In order to find a better balance between expressiveness and tractability, we combine these with the notion of determinism for regular expressions used in XML DTDs and XML Schema. This includes the definition of a suitable automaton model, and a generalization of the Glushkov construction. We demonstrate that, compared to their non-deterministic superclass, these deterministic regular expressions with back-references have desirable algorithmic properties (i.e., efficiently solvable membership problem and some decidable problems in static analysis), while, at the same time, their expressive power exceeds that of deterministic regular expressions without back-references.},
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   172
	author = {D.D.~Freydenberger and M.L.~Schmid},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   173
	doi = {https://doi.org/10.1016/j.jcss.2019.04.001},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   174
	issn = {0022-0000},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   175
	journal = {Journal of Computer and System Sciences},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   176
	keywords = {Deterministic regular expression, Regex, Glushkov automaton},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   177
	pages = {1-39},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   178
	title = {Deterministic regular expressions with back-references},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   179
	url = {https://www.sciencedirect.com/science/article/pii/S0022000018301818},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   180
	volume = {105},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   181
	year = {2019},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   182
	bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0022000018301818},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   183
	bdsk-url-2 = {https://doi.org/10.1016/j.jcss.2019.04.001}}
624
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   184
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   185
@inproceedings{Frey2013,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   186
	address = {Dagstuhl, Germany},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   187
	annote = {Keywords: extended regular expressions, regex, decidability, non-recursive tradeoffs},
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   188
	author = {D.D.~Freydenberger},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   189
	booktitle = {28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   190
	doi = {10.4230/LIPIcs.STACS.2011.507},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   191
	editor = {Thomas Schwentick and Christoph D{\"u}rr},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   192
	isbn = {978-3-939897-25-5},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   193
	issn = {1868-8969},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   194
	pages = {507--518},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   195
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   196
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   197
	title = {{Extended Regular Expressions: Succinctness and Decidability}},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   198
	url = {http://drops.dagstuhl.de/opus/volltexte/2011/3039},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   199
	urn = {urn:nbn:de:0030-drops-30396},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   200
	volume = {9},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   201
	year = {2011},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   202
	bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2011/3039},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   203
	bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.STACS.2011.507}}
624
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   204
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   205
@article{campeanu2003formal,
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   206
	author = {C.~C{\^a}mpeanu and K.~Salomaa and S.~Yu},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   207
	journal = {International Journal of Foundations of Computer Science},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   208
	number = {06},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   209
	pages = {1007--1018},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   210
	publisher = {World Scientific},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   211
	title = {A formal study of practical regular expressions},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   212
	volume = {14},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   213
	year = {2003}}
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   214
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   215
@article{campeanu2009patterns,
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   216
	author = {C.~C{\^a}mpeanu and N.~Santean},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   217
	doi = {10.1007/s00236-009-0090-y},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   218
	journal = {Acta Inf.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   219
	month = {05},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   220
	pages = {193-207},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   221
	title = {On the closure of pattern expressions languages under intersection with regular languages},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   222
	volume = {46},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   223
	year = {2009},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   224
	bdsk-url-1 = {https://doi.org/10.1007/s00236-009-0090-y}}
624
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   225
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   226
@article{CAMPEANU2009Intersect,
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   227
	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.},
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   228
	author = {C.~C{\^a}mpeanu and N.~Santean},
624
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   229
	doi = {https://doi.org/10.1016/j.tcs.2009.02.022},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   230
	issn = {0304-3975},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   231
	journal = {Theoretical Computer Science},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   232
	keywords = {Extended regular expression, Regex automata system, Regex},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   233
	note = {Formal Languages and Applications: A Collection of Papers in Honor of Sheng Yu},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   234
	number = {24},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   235
	pages = {2336-2344},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   236
	title = {On the intersection of regex languages with regular languages},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   237
	url = {https://www.sciencedirect.com/science/article/pii/S0304397509001789},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   238
	volume = {410},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   239
	year = {2009},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   240
	bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/S0304397509001789},
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   241
	bdsk-url-2 = {https://doi.org/10.1016/j.tcs.2009.02.022}}
8ffa28fce271 all comments incorporated!!+related work
Chengsong
parents: 622
diff changeset
   242
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   243
@incollection{Aho1990,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   244
	abstract = {Publisher Summary
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   245
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.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   246
	address = {Amsterdam},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   247
	author = {A.V.~Aho},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   248
	booktitle = {Algorithms and Complexity},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   249
	doi = {https://doi.org/10.1016/B978-0-444-88071-0.50010-2},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   250
	editor = {JAN {VAN LEEUWEN}},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   251
	isbn = {978-0-444-88071-0},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   252
	pages = {255-300},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   253
	publisher = {Elsevier},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   254
	series = {Handbook of Theoretical Computer Science},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   255
	title = {CHAPTER 5 - Algorithms for Finding Patterns in Strings},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   256
	url = {https://www.sciencedirect.com/science/article/pii/B9780444880710500102},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   257
	year = {1990},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   258
	bdsk-url-1 = {https://www.sciencedirect.com/science/article/pii/B9780444880710500102},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   259
	bdsk-url-2 = {https://doi.org/10.1016/B978-0-444-88071-0.50010-2}}
625
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   260
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   261
@inproceedings{Might2011,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   262
	abstract = {We present a functional approach to parsing unrestricted context-free grammars based on Brzozowski's derivative of regular expressions. If we consider context-free grammars as recursive regular expressions, Brzozowski's equational theory extends without modification to context-free grammars (and it generalizes to parser combinators). The supporting actors in this story are three concepts familiar to functional programmers - laziness, memoization and fixed points; these allow Brzozowski's original equations to be transliterated into purely functional code in about 30 lines spread over three functions.Yet, this almost impossibly brief implementation has a drawback: its performance is sour - in both theory and practice. The culprit? Each derivative can double the size of a grammar, and with it, the cost of the next derivative.Fortunately, much of the new structure inflicted by the derivative is either dead on arrival, or it dies after the very next derivative. To eliminate it, we once again exploit laziness and memoization to transliterate an equational theory that prunes such debris into working code. Thanks to this compaction, parsing times become reasonable in practice.We equip the functional programmer with two equational theories that, when combined, make for an abbreviated understanding and implementation of a system for parsing context-free languages.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   263
	address = {New York, NY, USA},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   264
	author = {M.~Might and D.~Darais and D.~Spiewak},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   265
	booktitle = {Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   266
	doi = {10.1145/2034773.2034801},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   267
	isbn = {9781450308656},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   268
	keywords = {derivative, parsing, context-free grammar, parser combinator, formal languages, regular expressions},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   269
	location = {Tokyo, Japan},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   270
	numpages = {7},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   271
	pages = {189--195},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   272
	publisher = {Association for Computing Machinery},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   273
	series = {ICFP '11},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   274
	title = {Parsing with Derivatives: A Functional Pearl},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   275
	url = {https://doi.org/10.1145/2034773.2034801},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   276
	year = {2011},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   277
	bdsk-url-1 = {https://doi.org/10.1145/2034773.2034801}}
625
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   278
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   279
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   280
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   281
@inproceedings{Adams2016,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   282
  title={On the complexity and performance of parsing with derivatives},
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   283
  author={M.D.~Adams and C.~Hollenbeck and M.~MightMatthew},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   284
  booktitle={Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   285
  pages={224--236},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   286
  year={2016}
625
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   287
}
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   288
@article{Huet1997,
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   289
author = {G.~Huet},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   290
title = {The Zipper},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   291
year = {1997},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   292
issue_date = {September 1997},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   293
publisher = {Cambridge University Press},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   294
address = {USA},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   295
volume = {7},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   296
number = {5},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   297
issn = {0956-7968},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   298
url = {https://doi.org/10.1017/S0956796897002864},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   299
doi = {10.1017/S0956796897002864},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   300
abstract = {Almost every programmer has faced the problem of representing a tree together with a subtree that is the focus of attention, where that focus may move left, right, up or down the tree. The Zipper is Huet's nifty name for a nifty data structure which fulfills this need. I wish I had known of it when I faced this task, because the solution I came up with was not quite so efficient or elegant as the Zipper.},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   301
journal = {J. Funct. Program.},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   302
month = {sep},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   303
pages = {549–554},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   304
numpages = {6}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   305
}
625
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   306
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   307
@article{Darragh2020,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   308
	abstract = {Parsing with Derivatives (PwD) is an elegant approach to parsing context-free grammars (CFGs). It takes the equational theory behind Brzozowski's derivative for regular expressions and augments that theory with laziness, memoization, and fixed points. The result is a simple parser for arbitrary CFGs. Although recent work improved the performance of PwD, it remains inefficient due to the algorithm repeatedly traversing some parts of the grammar. In this functional pearl, we show how to avoid this inefficiency by suspending the state of the traversal in a zipper. When subsequent derivatives are taken, we can resume the traversal from where we left off without retraversing already traversed parts of the grammar. However, the original zipper is designed for use with trees, and we want to parse CFGs. CFGs can include shared regions, cycles, and choices between alternates, which makes them incompatible with the traditional tree model for zippers. This paper develops a generalization of zippers to properly handle these additional features. Just as PwD generalized Brzozowski's derivatives from regular expressions to CFGs, we generalize Huet's zippers from trees to CFGs. Abstract The resulting parsing algorithm is concise and efficient: it takes only 31 lines of OCaml code to implement the derivative function but performs 6,500 times faster than the original PwD and 3.24 times faster than the optimized implementation of PwD.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   309
	address = {New York, NY, USA},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   310
	articleno = {108},
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   311
	author = {P.~Darragh and M.D.~Adams},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   312
	doi = {10.1145/3408990},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   313
	issue_date = {August 2020},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   314
	journal = {Proc. ACM Program. Lang.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   315
	keywords = {Derivatives, Zippers, Parsing with Derivatives, Parsing},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   316
	month = {aug},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   317
	number = {ICFP},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   318
	numpages = {28},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   319
	publisher = {Association for Computing Machinery},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   320
	title = {Parsing with Zippers (Functional Pearl)},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   321
	url = {https://doi.org/10.1145/3408990},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   322
	volume = {4},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   323
	year = {2020},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   324
	bdsk-url-1 = {https://doi.org/10.1145/3408990}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   325
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   326
@article{Edelmann2021,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   327
	abstract = {Parsing is the process that enables a computer system to  make sense of raw data. Parsing is common to almost all  computer systems: It is involved every time sequential data  is read and elaborated into structured data. The theory of  parsing usually focuses on the binary recognition aspect of  parsing and eschews this essential data-elaboration aspect.  In this thesis, I present a declarative framework for  value-aware parsing that explicitly integrates data  elaboration.
625
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   328
Within the framework of the thesis, I present  parsing algorithms that are based on the concept of  Brzozowski's derivatives. Derivative-based parsing  algorithms present several advantages: they are elegant,  amenable to formal reasoning, and easy to implement.  Unfortunately, the performance of these algorithms in  practice is often not competitive with other approaches. In  this thesis, I show a general technique inspired by Huet's  Zipper to greatly enhance the performance of  derivative-based algorithms, and I do so without  compromising their elegance, amenability to formal  reasoning, or ease of implementation.
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   329
First, I present a  technique for building efficient tokenisers that is based  on Brzozowski's derivatives and Huet's zipper and that does  not require the usual burdensome explicit conversion to  automata. I prove the technique is correct in Coq and  present SILEX, a Scala lexing library based on the  technique. I demonstrate that the approach is competitive  with state-of-the-art solutions.
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   330
Then, I present a  characterisation of LL(1) languages based on the concept of  should-not-follow sets. I present an algorithm for parsing  LL(1) languages with derivatives and zippers. I show a  formal proof of the algorithm's correctness and prove its  worst-case linear-time complexity. I show how the LL(1)  parsing with derivatives and zippers algorithm corresponds  to the traditional LL(1) parsing algorithm.
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   331
I then present  SCALL1ON, a Scala parsing combinators library for LL(1)  languages that incorporates the LL(1) parsing with  derivatives and zippers algorithm. I present an expressive  and familiar combinator-based interface for describing  LL(1) languages. I present techniques that help precisely  locate LL(1) conflicts in user code. I discuss several  advantages of the parsing with derivatives approach within  the context of a parsing library. I also present SCALL1ON's  enumeration and pretty-printing features and discuss their  implementation. Through a series of benchmarks, I  demonstrate the good performance and practicality of the  approach. Finally, I present how to adapt the LL(1) parsing  with derivatives and zippers algorithm to support arbitrary  context-free languages. I show how the adapted algorithm  corresponds to general parsing algorithms, such as Earley's  parsing algorithm.},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   332
	address = {Lausanne},
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   333
	author = {R.~Edelmann},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   334
	doi = {10.5075/epfl-thesis-7357},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   335
	institution = {IINFCOM},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   336
	pages = {246},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   337
	publisher = {EPFL},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   338
	title = {Efficient Parsing with Derivatives and Zippers},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   339
	url = {http://infoscience.epfl.ch/record/287059},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   340
	year = {2021},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   341
	bdsk-url-1 = {http://infoscience.epfl.ch/record/287059},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   342
	bdsk-url-2 = {https://doi.org/10.5075/epfl-thesis-7357}}
625
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   343
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   344
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   345
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   346
@inproceedings{Paulson2015,,
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   347
author = {L.~Paulson},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   348
year = {2015},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   349
month = {05},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   350
pages = {},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   351
title = {A Formalisation of Finite Automata Using Hereditarily Finite Sets},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   352
isbn = {978-3-319-21400-9},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   353
doi = {10.1007/978-3-319-21401-6_15}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   354
}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   355
625
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   356
@inproceedings{Zippy2020,
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   357
	abstract = {In this paper, we present an efficient, functional, and formally verified parsing algorithm for LL(1) context-free expressions based on the concept of derivatives of formal languages. Parsing with derivatives is an elegant parsing technique, which, in the general case, suffers from cubic worst-case time complexity and slow performance in practice. We specialise the parsing with derivatives algorithm to LL(1) context-free expressions, where alternatives can be chosen given a single token of lookahead. We formalise the notion of LL(1) expressions and show how to efficiently check the LL(1) property. Next, we present a novel linear-time parsing with derivatives algorithm for LL(1) expressions operating on a zipper-inspired data structure. We prove the algorithm correct in Coq and present an implementation as a part of Scallion, a parser combinators framework in Scala with enumeration and pretty printing capabilities.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   358
	address = {New York, NY, USA},
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   359
	author = {R.~Edelmannand H.~Jad and K.~Viktor},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   360
	booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   361
	doi = {10.1145/3385412.3385992},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   362
	isbn = {9781450376136},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   363
	keywords = {Parsing, Zipper, Formal proof, LL(1), Derivatives},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   364
	location = {London, UK},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   365
	numpages = {16},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   366
	pages = {1036--1051},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   367
	publisher = {Association for Computing Machinery},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   368
	series = {PLDI 2020},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   369
	title = {Zippy LL(1) Parsing with Derivatives},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   370
	url = {https://doi.org/10.1145/3385412.3385992},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   371
	year = {2020},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   372
	bdsk-url-1 = {https://doi.org/10.1145/3385412.3385992}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   373
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   374
@article{fowler2003,
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   375
	author = {G.~Fowler},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   376
	journal = {URL: https://web. archive. org/web/20050408073627/http://www. research. att. com/\~{} gsf/testregex/re-interpretation. html},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   377
	title = {An interpretation of the POSIX regex standard},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   378
	year = {2003}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   379
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   380
@inproceedings{Snort1999,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   381
	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.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   382
	address = {USA},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   383
	author = {M.~Roesch},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   384
	booktitle = {Proceedings of the 13th USENIX Conference on System Administration},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   385
	location = {Seattle, Washington},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   386
	numpages = {10},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   387
	pages = {229--238},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   388
	publisher = {USENIX Association},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   389
	series = {LISA '99},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   390
	title = {Snort - Lightweight Intrusion Detection for Networks},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   391
	year = {1999}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   392
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   393
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   394
@article{Reps1998,
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   395
author = {T.~Reps},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   396
title = {“Maximal-Munch” Tokenization in Linear Time},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   397
year = {1998},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   398
issue_date = {March 1998},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   399
publisher = {Association for Computing Machinery},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   400
address = {New York, NY, USA},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   401
volume = {20},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   402
number = {2},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   403
issn = {0164-0925},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   404
url = {https://doi.org/10.1145/276393.276394},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   405
doi = {10.1145/276393.276394},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   406
abstract = {The lexical-analysis (or scanning) phase of a compiler attempts to partition an input string into a sequence of tokens. The convention in most languages is that the input is scanned left to right, and each token identified is a “maximal munch” of the remaining input—the longest prefix of the remaining input that is a token of the language. Although most of the standard compiler textbooks present a way to perform maximal-munch tokenization, the algorithm they describe is one that, for certain sets of token definitions, can cause the scanner to exhibit quadratic behavior in the worst case. In the article, we show that maximal-munch tokenization can always be performed in time linear in the size of the input.},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   407
journal = {ACM Trans. Program. Lang. Syst.},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   408
month = {mar},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   409
pages = {259–273},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   410
numpages = {15},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   411
keywords = {backtracking, tokenization, tabulation, dynamic programming, memoization}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   412
}
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   413
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   414
@inproceedings{Bro,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   415
author = {V.~Paxson},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   416
title = {Bro: A System for Detecting Network Intruders in Real-Time},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   417
year = {1998},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   418
publisher = {USENIX Association},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   419
address = {USA},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   420
abstract = {We describe Bro, a stand-alone system for detecting network intruders in real-time by passively monitoring a network link over which the intruder's traffic transits. We give an overview of the system's design, which emphasizes high-speed (FDDI-rate) monitoring, real-time notification, clear separation between mechanism and policy, and extensibility. To achieve these ends, Bro is divided into an "event engine" that reduces a kernel-filtered network traffic stream into a series of higher-level events, and a "policy script interpreter" that interprets event handlers written in a specialized language used to express a site's security policy. Event handlers can update state information, synthesize new events, record information to disk, and generate real-time notifications via syslog. We also discuss a number of attacks that attempt to subvert passive monitoring systems and defenses against these, and give particulars of how Bro analyzes the four applications integrated into it so far: Finger, FTP, Portmapper and Telnet. The system is publicly available in source code form.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   421
booktitle = {Proceedings of the 7th Conference on USENIX Security Symposium - Volume 7},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   422
pages = {3},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   423
numpages = {1},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   424
location = {San Antonio, Texas},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   425
series = {SSYM'98}
625
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   426
}
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   427
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   428
@INPROCEEDINGS{Sidhu2001,
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   429
  author={Sidhu, R. and Prasanna, V.K.},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   430
  booktitle={The 9th Annual IEEE Symposium on Field-Programmable Custom Computing Machines (FCCM'01)}, 
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   431
  title={Fast Regular Expression Matching Using FPGAs}, 
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   432
  year={2001},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   433
  volume={},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   434
  number={},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   435
  pages={227-238},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   436
  doi={}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   437
}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   438
@article{Turonova2020,
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   439
author = {L.~Turo\v{n}ov\'{a} and L.~Hol\'{\i}k  and O.~Leng\'{a}l and O.~Saarikivi and M.~Veanes and T.~Vojnar },
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   440
title = {Regex Matching with Counting-Set Automata},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   441
year = {2020},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   442
issue_date = {November 2020},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   443
publisher = {Association for Computing Machinery},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   444
address = {New York, NY, USA},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   445
volume = {4},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   446
number = {OOPSLA},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   447
url = {https://doi.org/10.1145/3428286},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   448
doi = {10.1145/3428286},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   449
abstract = {We propose a solution to the problem of efficient matching regular expressions (regexes) with bounded repetition, such as (ab){1,100}, using deterministic automata. For this, we introduce novel counting-set automata (CsAs), automata with registers that can hold sets of bounded integers and can be manipulated by a limited portfolio of constant-time operations. We present an algorithm that compiles a large sub-class of regexes to deterministic CsAs. This includes (1) a novel Antimirov-style translation of regexes with counting to counting automata (CAs), nondeterministic automata with bounded counters, and (2) our main technical contribution, a determinization of CAs that outputs CsAs. The main advantage of this workflow is that the size of the produced CsAs does not depend on the repetition bounds used in the regex (while the size of the DFA is exponential to them). Our experimental results confirm that deterministic CsAs produced from practical regexes with repetition are indeed vastly smaller than the corresponding DFAs. More importantly, our prototype matcher based on CsA simulation handles practical regexes with repetition regardless of sizes of counter bounds. It easily copes with regexes with repetition where state-of-the-art matchers struggle.},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   450
journal = {Proc. ACM Program. Lang.},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   451
month = {nov},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   452
articleno = {218},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   453
numpages = {30},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   454
keywords = {counting-set automata, counting automata, bounded repetition, ReDos, Antimirov's derivatives, regular expression matching, determinization}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   455
}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   456
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   457
@inproceedings{Kumar2006,
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   458
author = {S.~Kumar and S.~Dharmapurikar and F.~Yu and P.~Crowley and J.~Turner},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   459
title = {Algorithms to Accelerate Multiple Regular Expressions Matching for Deep Packet Inspection},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   460
year = {2006},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   461
isbn = {1595933085},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   462
publisher = {Association for Computing Machinery},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   463
address = {New York, NY, USA},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   464
url = {https://doi.org/10.1145/1159913.1159952},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   465
doi = {10.1145/1159913.1159952},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   466
abstract = {There is a growing demand for network devices capable of examining the content of data packets in order to improve network security and provide application-specific services. Most high performance systems that perform deep packet inspection implement simple string matching algorithms to match packets against a large, but finite set of strings. owever, there is growing interest in the use of regular expression-based pattern matching, since regular expressions offer superior expressive power and flexibility. Deterministic finite automata (DFA) representations are typically used to implement regular expressions. However, DFA representations of regular expression sets arising in network applications require large amounts of memory, limiting their practical application.In this paper, we introduce a new representation for regular expressions, called the Delayed Input DFA (D2FA), which substantially reduces space equirements as compared to a DFA. A D2FA is constructed by transforming a DFA via incrementally replacing several transitions of the automaton with a single default transition. Our approach dramatically reduces the number of distinct transitions between states. For a collection of regular expressions drawn from current commercial and academic systems, a D2FA representation reduces transitions by more than 95%. Given the substantially reduced space equirements, we describe an efficient architecture that can perform deep packet inspection at multi-gigabit rates. Our architecture uses multiple on-chip memories in such a way that each remains uniformly occupied and accessed over a short duration, thus effectively distributing the load and enabling high throughput. Our architecture can provide ostffective packet content scanning at OC-192 rates with memory requirements that are consistent with current ASIC technology.},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   467
booktitle = {Proceedings of the 2006 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   468
pages = {339–350},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   469
numpages = {12},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   470
keywords = {regular expressions, DFA, deep packet inspection},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   471
location = {Pisa, Italy},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   472
series = {SIGCOMM '06}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   473
}
625
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   474
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   475
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   476
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   477
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   478
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   479
@inproceedings{Becchi2007,
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   480
author = {M.~Becchi and P.~Crowley},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   481
title = {An Improved Algorithm to Accelerate Regular Expression Evaluation},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   482
year = {2007},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   483
isbn = {9781595939456},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   484
publisher = {Association for Computing Machinery},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   485
address = {New York, NY, USA},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   486
url = {https://doi.org/10.1145/1323548.1323573},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   487
doi = {10.1145/1323548.1323573},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   488
abstract = {Modern network intrusion detection systems need to perform regular expression matching at line rate in order to detect the occurrence of critical patterns in packet payloads. While deterministic finite automata (DFAs) allow this operation to be performed in linear time, they may exhibit prohibitive memory requirements. In [9], Kumar et al. propose Delayed Input DFAs (D2FAs), which provide a trade-off between the memory requirements of the compressed DFA and the number of states visited for each character processed, which corresponds directly to the memory bandwidth required to evaluate regular expressions.In this paper we introduce a general compression technique that results in at most 2N state traversals when processing a string of length N. In comparison to the D2FA approach, our technique achieves comparable levels of compression, with lower provable bounds on memory bandwidth (or greater compression for a given bandwidth bound). Moreover, our proposed algorithm has lower complexity, is suitable for scenarios where a compressed DFA needs to be dynamically built or updated, and fosters locality in the traversal process. Finally, we also describe a novel alphabet reduction scheme for DFA-based structures that can yield further dramatic reductions in data structure size.},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   489
booktitle = {Proceedings of the 3rd ACM/IEEE Symposium on Architecture for Networking and Communications Systems},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   490
pages = {145–154},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   491
numpages = {10},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   492
keywords = {regular expressions, DFA, deep packet inspection},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   493
location = {Orlando, Florida, USA},
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   494
series = {ANCS '07}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   495
}
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   496
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   497
@inproceedings{Becchi08,
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   498
	author = {M.~Becchi and , Patrick},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   499
	doi = {10.1145/1544012.1544037},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   500
	month = {01},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   501
	pages = {25},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   502
	title = {Extending finite automata to efficiently match Perl-compatible regular expressions},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   503
	year = {2008},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   504
	bdsk-url-1 = {https://doi.org/10.1145/1544012.1544037}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   505
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   506
@book{Sakarovitch2009,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   507
	author = {Sakarovitch, Jacques},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   508
	doi = {10.1017/CBO9781139195218},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   509
	editor = {Thomas, ReubenTranslator},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   510
	place = {Cambridge},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   511
	publisher = {Cambridge University Press},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   512
	title = {Elements of Automata Theory},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   513
	year = {2009},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   514
	bdsk-url-1 = {https://doi.org/10.1017/CBO9781139195218}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   515
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   516
@unpublished{CSL2022,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   517
	author = {Chengsong Tan and Christian Urban},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   518
	note = {submitted},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   519
	title = {POSIX Lexing with Bitcoded Derivatives}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   520
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   521
@inproceedings{Verbatim,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   522
	author = {Egolf, Derek and Lasser, Sam and Fisher, Kathleen},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   523
	booktitle = {2021 IEEE Security and Privacy Workshops (SPW)},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   524
	doi = {10.1109/SPW53761.2021.00022},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   525
	pages = {92-100},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   526
	title = {Verbatim: A Verified Lexer Generator},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   527
	year = {2021},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   528
	bdsk-url-1 = {https://doi.org/10.1109/SPW53761.2021.00022}}
625
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   529
b797c9a709d9 section reorganising, related work
Chengsong
parents: 624
diff changeset
   530
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   531
@inproceedings{Nipkow1998,
627
94db2636a296 finished!
Chengsong
parents: 626
diff changeset
   532
  author    = {T.~Nipkow},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   533
  editor    = {Jim Grundy and
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   534
               Malcolm C. Newey},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   535
  title     = {Verified Lexical Analysis},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   536
  booktitle = {Theorem Proving in Higher Order Logics, 11th International Conference,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   537
               TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   538
  series    = {Lecture Notes in Computer Science},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   539
  volume    = {1479},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   540
  pages     = {1--15},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   541
  publisher = {Springer},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   542
  year      = {1998},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   543
  url       = {https://doi.org/10.1007/BFb0055126},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   544
  doi       = {10.1007/BFb0055126},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   545
  timestamp = {Tue, 14 May 2019 10:00:48 +0200},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   546
  biburl    = {https://dblp.org/rec/conf/tphol/Nipkow98.bib},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   547
  bibsource = {dblp computer science bibliography, https://dblp.org}
607
e6fc9b72c0e3 chap1 almost done
Chengsong
parents: 606
diff changeset
   548
}
e6fc9b72c0e3 chap1 almost done
Chengsong
parents: 606
diff changeset
   549
e6fc9b72c0e3 chap1 almost done
Chengsong
parents: 606
diff changeset
   550
601
Chengsong
parents: 518
diff changeset
   551
@inproceedings{Verbatimpp,
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   552
	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.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   553
	address = {New York, NY, USA},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   554
	author = {Egolf, Derek and Lasser, Sam and Fisher, Kathleen},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   555
	booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   556
	doi = {10.1145/3497775.3503694},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   557
	isbn = {9781450391825},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   558
	keywords = {Brzozowski derivatives, formal verification, lexical analysis, semantic actions},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   559
	location = {Philadelphia, PA, USA},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   560
	numpages = {13},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   561
	pages = {27--39},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   562
	publisher = {Association for Computing Machinery},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   563
	series = {CPP 2022},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   564
	title = {Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   565
	url = {https://doi.org/10.1145/3497775.3503694},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   566
	year = {2022},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   567
	bdsk-url-1 = {https://doi.org/10.1145/3497775.3503694}}
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   568
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   569
@article{Turo_ov__2020,
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   570
	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
   571
	date-added = {2022-05-23 18:43:04 +0100},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   572
	date-modified = {2022-05-23 18:43:04 +0100},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   573
	doi = {10.1145/3428286},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   574
	journal = {Proceedings of the {ACM} on Programming Languages},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   575
	month = {nov},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   576
	number = {{OOPSLA}},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   577
	pages = {1--30},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   578
	publisher = {Association for Computing Machinery ({ACM})},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   579
	title = {Regex matching with counting-set automata},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   580
	url = {https://doi.org/10.1145%2F3428286},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   581
	volume = {4},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   582
	year = 2020,
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   583
	bdsk-url-1 = {https://doi.org/10.1145%2F3428286},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   584
	bdsk-url-2 = {https://doi.org/10.1145/3428286}}
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   585
468
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   586
@article{Rathnayake2014StaticAF,
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   587
	author = {Asiri Rathnayake and Hayo Thielecke},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   588
	journal = {ArXiv},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   589
	title = {Static Analysis for Regular Expression Exponential Runtime via Substructural Logics},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   590
	volume = {abs/1405.7058},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   591
	year = {2014}}
468
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   592
472
Chengsong
parents: 471
diff changeset
   593
@inproceedings{Weideman2017Static,
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   594
	author = {Nicolaas Weideman},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   595
	title = {Static analysis of regular expressions},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   596
	year = {2017}}
472
Chengsong
parents: 471
diff changeset
   597
468
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   598
@inproceedings{RibeiroAgda2017,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   599
	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
   600
	address = {New York, NY, USA},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   601
	articleno = {4},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   602
	author = {Ribeiro, Rodrigo and Bois, Andr\'{e} Du},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   603
	booktitle = {Proceedings of the 21st Brazilian Symposium on Programming Languages},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   604
	date-modified = {2022-03-16 16:38:47 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   605
	doi = {10.1145/3125374.3125381},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   606
	isbn = {9781450353892},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   607
	keywords = {Certified algorithms, regular expressions, dependent types, bit-codes},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   608
	location = {Fortaleza, CE, Brazil},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   609
	numpages = {8},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   610
	publisher = {Association for Computing Machinery},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   611
	series = {SBLP 2017},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   612
	title = {Certified Bit-Coded Regular Expression Parsing},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   613
	url = {https://doi.org/10.1145/3125374.3125381},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   614
	year = {2017},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   615
	bdsk-url-1 = {https://doi.org/10.1145/3125374.3125381}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   616
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   617
@article{Thompson_1968,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   618
	author = {Ken Thompson},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   619
	date-added = {2022-02-23 13:44:42 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   620
	date-modified = {2022-02-23 13:44:42 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   621
	doi = {10.1145/363347.363387},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   622
	journal = {Communications of the {ACM}},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   623
	month = {jun},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   624
	number = {6},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   625
	pages = {419--422},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   626
	publisher = {Association for Computing Machinery ({ACM})},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   627
	title = {Programming Techniques: Regular expression search algorithm},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   628
	url = {https://doi.org/10.1145%2F363347.363387},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   629
	volume = {11},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   630
	year = 1968,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   631
	bdsk-url-1 = {https://doi.org/10.1145%2F363347.363387},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   632
	bdsk-url-2 = {https://doi.org/10.1145/363347.363387}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   633
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   634
@article{17Bir,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   635
	author = {Asiri Rathnayake and Hayo Thielecke},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   636
	date-added = {2019-08-18 17:57:30 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   637
	date-modified = {2019-08-18 18:00:13 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   638
	journal = {arXiv:1405.7058},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   639
	title = {Static Analysis for Regular Expression Exponential Runtime via Substructural Logics},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   640
	year = {2017}}
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   641
471
Chengsong
parents: 468
diff changeset
   642
@article{alfred2014algorithms,
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   643
	author = {Alfred, V},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   644
	journal = {Algorithms and Complexity},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   645
	pages = {255},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   646
	publisher = {Elsevier},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   647
	title = {Algorithms for finding patterns in strings},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   648
	volume = {1},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   649
	year = {2014}}
471
Chengsong
parents: 468
diff changeset
   650
468
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   651
@article{nielson11bcre,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   652
	author = {Lasse Nielsen, Fritz Henglein},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   653
	date-added = {2019-07-03 21:09:39 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   654
	date-modified = {2019-07-03 21:17:33 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   655
	journal = {LATA},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   656
	title = {Bit-coded Regular Expression Parsing},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   657
	year = {2011},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   658
	bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxA1Li4vLi4vLi4vTXkgTWFjIChNYWNCb29rLVBybykvRGVza3RvcC9mcml0ei1wYXBlci5wZGZPEQF+AAAAAAF+AAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8PZnJpdHotcGFwZXIucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAMAAAogY3UAAAAAAAAAAAAAAAAAB0Rlc2t0b3AAAAIAQi86VXNlcnM6Y3N0YW46RHJvcGJveDpNeSBNYWMgKE1hY0Jvb2stUHJvKTpEZXNrdG9wOmZyaXR6LXBhcGVyLnBkZgAOACAADwBmAHIAaQB0AHoALQBwAGEAcABlAHIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAEBVc2Vycy9jc3Rhbi9Ecm9wYm94L015IE1hYyAoTWFjQm9vay1Qcm8pL0Rlc2t0b3AvZnJpdHotcGFwZXIucGRmABMAAS8AABUAAgAM//8AAAAIAA0AGgAkAFwAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAAB3g==}}
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   659
468
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   660
@software{regexploit2021,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   661
	author = {Ben Caller, Luca Carettoni},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   662
	date-added = {2020-11-24 00:00:00 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   663
	date-modified = {2021-05-07 00:00:00 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   664
	keywords = {ReDos static analyser},
472
Chengsong
parents: 471
diff changeset
   665
	month = {May},
Chengsong
parents: 471
diff changeset
   666
	title = {regexploit},
Chengsong
parents: 471
diff changeset
   667
	url = {https://github.com/doyensec/regexploit},
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   668
	year = {2021},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   669
	bdsk-url-1 = {https://github.com/doyensec/regexploit}}
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   670
608
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   671
@software{pcre,
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   672
	author = {Philip Hazel},
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   673
	date-added = {1997-01-01 00:00:00 +0000},
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   674
	date-modified = {2021-06-14 00:00:00 +0000},
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   675
	keywords = {Perl Compatible Regular Expressions},
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   676
	month = {June},
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   677
	title = {PCRE},
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   678
	url = {https://www.pcre.org/original/doc/html/},
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   679
	year = {2021},
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   680
	bdsk-url-1 = {https://www.pcre.org/original/doc/html/}}
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   681
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   682
@misc{communityRules,
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   683
	howpublished = {\url{https://www.snort.org/faq/what-are-community-rules}},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   684
	note = {[Online; last accessed 19-November-2022]},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   685
	title = {{Snort Community Rules}},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   686
	year = {2022}}
608
37b6fd310a16 added related work chap
Chengsong
parents: 607
diff changeset
   687
471
Chengsong
parents: 468
diff changeset
   688
@misc{KuklewiczHaskell,
Chengsong
parents: 468
diff changeset
   689
	author = {Kuklewicz},
Chengsong
parents: 468
diff changeset
   690
	keywords = {Buggy C POSIX Lexing Libraries},
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   691
	title = {Regex Posix},
471
Chengsong
parents: 468
diff changeset
   692
	url = {https://wiki.haskell.org/Regex_Posix},
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   693
	year = {2017},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   694
	bdsk-url-1 = {https://wiki.haskell.org/Regex_Posix}}
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   695
472
Chengsong
parents: 471
diff changeset
   696
@misc{regex101,
Chengsong
parents: 471
diff changeset
   697
	author = {Firas Dib},
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   698
	keywords = {regex tester debugger},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   699
	title = {regex101},
472
Chengsong
parents: 471
diff changeset
   700
	url = {https://regex101.com/},
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   701
	year = {2011},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   702
	bdsk-url-1 = {https://regex101.com/}}
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   703
500
Chengsong
parents: 472
diff changeset
   704
@misc{atomEditor,
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   705
	author = {Dunno},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   706
	keywords = {text editor},
500
Chengsong
parents: 472
diff changeset
   707
	title = {Atom Editor},
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   708
	url = {https://atom.io},
500
Chengsong
parents: 472
diff changeset
   709
	year = {2022},
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   710
	bdsk-url-1 = {https://atom.io}}
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   711
471
Chengsong
parents: 468
diff changeset
   712
@techreport{grathwohl2014crash,
518
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   713
	author = {Grathwohl, Niels Bj{\o}rn Bugge and Henglein, Fritz and Rasmussen, Ulrik Terp},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   714
	institution = {Technical report, University of Copenhagen},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   715
	title = {A Crash-Course in Regular Expression Parsing and Regular Expressions as Types},
ff7945a988a3 more to thesis
Chengsong
parents: 500
diff changeset
   716
	year = {2014}}
471
Chengsong
parents: 468
diff changeset
   717
602
Chengsong
parents: 601
diff changeset
   718
@inproceedings{xml2015,
626
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   719
	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.},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   720
	address = {New York, NY, USA},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   721
	author = {Bj\"{o}rklund, Henrik and Martens, Wim and Timm, Thomas},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   722
	booktitle = {Proceedings of the 24th ACM International on Conference on Information and Knowledge Management},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   723
	doi = {10.1145/2806416.2806434},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   724
	isbn = {9781450337946},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   725
	keywords = {regular expressions, schema, regular path queries, xml},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   726
	location = {Melbourne, Australia},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   727
	numpages = {10},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   728
	pages = {1541--1550},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   729
	publisher = {Association for Computing Machinery},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   730
	series = {CIKM '15},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   731
	title = {Efficient Incremental Evaluation of Succinct Regular Expressions},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   732
	url = {https://doi.org/10.1145/2806416.2806434},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   733
	year = {2015},
1c8525061545 finished!
Chengsong
parents: 625
diff changeset
   734
	bdsk-url-1 = {https://doi.org/10.1145/2806416.2806434}}
602
Chengsong
parents: 601
diff changeset
   735
468
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   736
@misc{SE16,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   737
	author = {StackStatus},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   738
	date-added = {2019-06-26 11:28:41 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   739
	date-modified = {2019-06-26 16:07:31 +0000},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   740
	keywords = {ReDos Attack},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   741
	month = {July},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   742
	rating = {5},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   743
	read = {1},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   744
	title = {Stack Overflow Outage Postmortem},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   745
	url = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   746
	year = {2016},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   747
	bdsk-url-1 = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   748
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   749
@article{HosoyaVouillonPierce2005,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   750
	author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   751
	journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   752
	number = 1,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   753
	pages = {46--90},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   754
	title = {{R}egular {E}xpression {T}ypes for {XML}},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   755
	volume = 27,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   756
	year = {2005}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   757
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   758
@misc{POSIX,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   759
	note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   760
	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
   761
	year = {2004}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   762
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   763
@inproceedings{AusafDyckhoffUrban2016,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   764
	author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   765
	booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   766
	pages = {69--86},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   767
	series = {LNCS},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   768
	title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   769
	volume = {9807},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   770
	year = {2016}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   771
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   772
@article{aduAFP16,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   773
	author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   774
	issn = {2150-914x},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   775
	journal = {Archive of Formal Proofs},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   776
	note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   777
	title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   778
	year = 2016}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   779
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   780
@techreport{CrashCourse2014,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   781
	annote = {draft report},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   782
	author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   783
	institution = {University of Copenhagen},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   784
	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
   785
	year = {2014}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   786
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   787
@inproceedings{Sulzmann2014,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   788
	author = {M.~Sulzmann and K.~Lu},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   789
	booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   790
	pages = {203--220},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   791
	series = {LNCS},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   792
	title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   793
	volume = {8475},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   794
	year = {2014}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   795
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   796
@inproceedings{Sulzmann2014b,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   797
	author = {M.~Sulzmann and P.~van Steenhoven},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   798
	booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   799
	pages = {174--191},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   800
	series = {LNCS},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   801
	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
   802
	volume = {8409},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   803
	year = {2014}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   804
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   805
@book{Pierce2015,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   806
	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
   807
	note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   808
	publisher = {Electronic textbook},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   809
	title = {{S}oftware {F}oundations},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   810
	year = {2015}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   811
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   812
@misc{Kuklewicz,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   813
	author = {C.~Kuklewicz},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   814
	howpublished = {\url{https://wiki.haskell.org/Regex_Posix}},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   815
	title = {{R}egex {P}osix}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   816
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   817
@article{Vansummeren2006,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   818
	author = {S.~Vansummeren},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   819
	journal = {ACM Transactions on Programming Languages and Systems},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   820
	number = {3},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   821
	pages = {389--428},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   822
	title = {{T}ype {I}nference for {U}nique {P}attern {M}atching},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   823
	volume = {28},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   824
	year = {2006}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   825
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   826
@inproceedings{Asperti12,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   827
	author = {A.~Asperti},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   828
	booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   829
	pages = {283--298},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   830
	series = {LNCS},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   831
	title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   832
	volume = {7406},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   833
	year = {2012}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   834
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   835
@inproceedings{Frisch2004,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   836
	author = {A.~Frisch and L.~Cardelli},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   837
	booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   838
	pages = {618--629},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   839
	series = {LNCS},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   840
	title = {{G}reedy {R}egular {E}xpression {M}atching},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   841
	volume = {3142},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   842
	year = {2004}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   843
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   844
@article{Antimirov95,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   845
	author = {V.~Antimirov},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   846
	journal = {Theoretical Computer Science},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   847
	pages = {291--319},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   848
	title = {{P}artial {D}erivatives of {R}egular {E}xpressions and {F}inite {A}utomata {C}onstructions},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   849
	volume = {155},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   850
	year = {1995}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   851
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   852
@inproceedings{Nipkow98,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   853
	author = {T.~Nipkow},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   854
	booktitle = {Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   855
	pages = {1--15},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   856
	series = {LNCS},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   857
	title = {{V}erified {L}exical {A}nalysis},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   858
	volume = 1479,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   859
	year = 1998}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   860
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   861
@article{Brzozowski1964,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   862
	author = {J.~A.~Brzozowski},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   863
	journal = {Journal of the {ACM}},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   864
	number = {4},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   865
	pages = {481--494},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   866
	title = {{D}erivatives of {R}egular {E}xpressions},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   867
	volume = {11},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   868
	year = {1964}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   869
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   870
@article{Leroy2009,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   871
	author = {X.~Leroy},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   872
	journal = {Communications of the ACM},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   873
	number = 7,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   874
	pages = {107--115},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   875
	title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   876
	volume = 52,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   877
	year = 2009}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   878
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   879
@inproceedings{Paulson2015,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   880
	author = {L.~C.~Paulson},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   881
	booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   882
	pages = {231--245},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   883
	series = {LNAI},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   884
	title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   885
	volume = {9195},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   886
	year = {2015}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   887
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   888
@article{Wu2014,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   889
	author = {C.~Wu and X.~Zhang and C.~Urban},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   890
	journal = {Journal of Automatic Reasoning},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   891
	number = {4},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   892
	pages = {451--480},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   893
	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
   894
	volume = {52},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   895
	year = {2014}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   896
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   897
@inproceedings{Regehr2011,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   898
	author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   899
	booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   900
	pages = {283--294},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   901
	title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   902
	year = {2011}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   903
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   904
@article{Norrish2014,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   905
	author = {A.~Barthwal and M.~Norrish},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   906
	journal = {Journal of Computer and System Sciences},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   907
	number = {2},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   908
	pages = {346--362},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   909
	title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   910
	volume = {80},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   911
	year = {2014}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   912
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   913
@article{Thompson1968,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   914
	author = {K.~Thompson},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   915
	issue_date = {June 1968},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   916
	journal = {Communications of the ACM},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   917
	number = {6},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   918
	pages = {419--422},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   919
	title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   920
	volume = {11},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   921
	year = {1968}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   922
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   923
@article{Owens2009,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   924
	author = {S.~Owens and J.~H.~Reppy and A.~Turon},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   925
	journal = {Journal of Functinal Programming},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   926
	number = {2},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   927
	pages = {173--190},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   928
	title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   929
	volume = {19},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   930
	year = {2009}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   931
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   932
@inproceedings{Sulzmann2015,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   933
	author = {M.~Sulzmann and P.~Thiemann},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   934
	booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory and Applications (LATA)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   935
	pages = {275--286},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   936
	series = {LNCS},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   937
	title = {{D}erivatives for {R}egular {S}huffle {E}xpressions},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   938
	volume = {8977},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   939
	year = {2015}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   940
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   941
@inproceedings{Chen2012,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   942
	author = {H.~Chen and S.~Yu},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   943
	booktitle = {Proc.~in the International Workshop on Theoretical Computer Science (WTCS)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   944
	pages = {343--356},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   945
	series = {LNCS},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   946
	title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   947
	volume = {7160},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   948
	year = {2012}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   949
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   950
@article{Krauss2011,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   951
	author = {A.~Krauss and T.~Nipkow},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   952
	journal = {Journal of Automated Reasoning},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   953
	pages = {95--106},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   954
	title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   955
	volume = 49,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   956
	year = 2012}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   957
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   958
@inproceedings{Traytel2015,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   959
	author = {D.~Traytel},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   960
	booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   961
	pages = {487--503},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   962
	series = {LIPIcs},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   963
	title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   964
	volume = {41},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   965
	year = {2015}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   966
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   967
@inproceedings{Traytel2013,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   968
	author = {D.~Traytel and T.~Nipkow},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   969
	booktitle = {Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   970
	pages = {3-12},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   971
	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
   972
	year = 2013}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   973
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   974
@inproceedings{Coquand2012,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   975
	author = {T.~Coquand and V.~Siles},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   976
	booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   977
	pages = {119--134},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   978
	series = {LNCS},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   979
	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
   980
	volume = {7086},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   981
	year = {2011}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   982
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   983
@inproceedings{Almeidaetal10,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   984
	author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   985
	booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   986
	pages = {59-68},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   987
	series = {LNCS},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   988
	title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   989
	volume = {6482},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   990
	year = {2010}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   991
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   992
@article{Owens2008,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   993
	author = {S.~Owens and K.~Slind},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   994
	journal = {Higher-Order and Symbolic Computation},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   995
	number = {4},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   996
	pages = {377--409},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   997
	title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   998
	volume = {21},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
   999
	year = {2008}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1000
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1001
@article{Owens2,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1002
	author = {S.~Owens and K.~Slind},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1003
	bibsource = {dblp computer science bibliography, http://dblp.org},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1004
	biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1005
	doi = {10.1007/s10990-008-9038-0},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1006
	journal = {Higher-Order and Symbolic Computation},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1007
	number = {4},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1008
	pages = {377--409},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1009
	timestamp = {Wed, 16 Dec 2009 13:51:02 +0100},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1010
	title = {Adapting functional programs to higher order logic},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1011
	url = {http://dx.doi.org/10.1007/s10990-008-9038-0},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1012
	volume = {21},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1013
	year = {2008},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1014
	bdsk-url-1 = {http://dx.doi.org/10.1007/s10990-008-9038-0}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1015
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1016
@misc{PCRE,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1017
	title = {{PCRE - Perl Compatible Regular Expressions}},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1018
	url = {http://www.pcre.org},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1019
	bdsk-url-1 = {http://www.pcre.org}}
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1020
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1021
@inproceedings{Davis18,
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1022
	author = {J.~C.~Davis and C.~.A.~Coghlan and F.~Servant and D.~Lee},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1023
	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
  1024
	numpages = {11},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1025
	pages = {246--256},
a0f27e21b42c all texrelated
Chengsong
parents:
diff changeset
  1026
	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
  1027
	year = {2018}}