|
1 %% This BibTeX bibliography file was created using BibDesk. |
|
2 %% https://bibdesk.sourceforge.io/ |
|
3 |
|
4 %% Created for CS TAN at 2022-03-16 16:38:47 +0000 |
|
5 |
|
6 |
|
7 %% Saved with string encoding Unicode (UTF-8) |
|
8 |
|
9 @article{Rathnayake2014StaticAF, |
|
10 title={Static Analysis for Regular Expression Exponential Runtime via Substructural Logics}, |
|
11 author={Asiri Rathnayake and Hayo Thielecke}, |
|
12 journal={ArXiv, |
|
13 year={2014}, |
|
14 volume={abs/1405.7058} |
|
15 } |
|
16 |
|
17 @inproceedings{RibeiroAgda2017, |
|
18 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.}, |
|
19 address = {New York, NY, USA}, |
|
20 articleno = {4}, |
|
21 author = {Ribeiro, Rodrigo and Bois, Andr\'{e} Du}, |
|
22 booktitle = {Proceedings of the 21st Brazilian Symposium on Programming Languages}, |
|
23 date-modified = {2022-03-16 16:38:47 +0000}, |
|
24 doi = {10.1145/3125374.3125381}, |
|
25 isbn = {9781450353892}, |
|
26 keywords = {Certified algorithms, regular expressions, dependent types, bit-codes}, |
|
27 location = {Fortaleza, CE, Brazil}, |
|
28 numpages = {8}, |
|
29 publisher = {Association for Computing Machinery}, |
|
30 series = {SBLP 2017}, |
|
31 title = {Certified Bit-Coded Regular Expression Parsing}, |
|
32 url = {https://doi.org/10.1145/3125374.3125381}, |
|
33 year = {2017}, |
|
34 bdsk-url-1 = {https://doi.org/10.1145/3125374.3125381}} |
|
35 |
|
36 @article{Thompson_1968, |
|
37 author = {Ken Thompson}, |
|
38 date-added = {2022-02-23 13:44:42 +0000}, |
|
39 date-modified = {2022-02-23 13:44:42 +0000}, |
|
40 doi = {10.1145/363347.363387}, |
|
41 journal = {Communications of the {ACM}}, |
|
42 month = {jun}, |
|
43 number = {6}, |
|
44 pages = {419--422}, |
|
45 publisher = {Association for Computing Machinery ({ACM})}, |
|
46 title = {Programming Techniques: Regular expression search algorithm}, |
|
47 url = {https://doi.org/10.1145%2F363347.363387}, |
|
48 volume = {11}, |
|
49 year = 1968, |
|
50 bdsk-url-1 = {https://doi.org/10.1145%2F363347.363387}, |
|
51 bdsk-url-2 = {https://doi.org/10.1145/363347.363387}} |
|
52 |
|
53 @article{17Bir, |
|
54 author = {Asiri Rathnayake and Hayo Thielecke}, |
|
55 date-added = {2019-08-18 17:57:30 +0000}, |
|
56 date-modified = {2019-08-18 18:00:13 +0000}, |
|
57 journal = {arXiv:1405.7058}, |
|
58 title = {Static Analysis for Regular Expression Exponential Runtime via Substructural Logics}, |
|
59 year = {2017}} |
|
60 |
|
61 @article{nielson11bcre, |
|
62 author = {Lasse Nielsen, Fritz Henglein}, |
|
63 date-added = {2019-07-03 21:09:39 +0000}, |
|
64 date-modified = {2019-07-03 21:17:33 +0000}, |
|
65 journal = {LATA}, |
|
66 title = {Bit-coded Regular Expression Parsing}, |
|
67 year = {2011}, |
|
68 bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxA1Li4vLi4vLi4vTXkgTWFjIChNYWNCb29rLVBybykvRGVza3RvcC9mcml0ei1wYXBlci5wZGZPEQF+AAAAAAF+AAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8PZnJpdHotcGFwZXIucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAMAAAogY3UAAAAAAAAAAAAAAAAAB0Rlc2t0b3AAAAIAQi86VXNlcnM6Y3N0YW46RHJvcGJveDpNeSBNYWMgKE1hY0Jvb2stUHJvKTpEZXNrdG9wOmZyaXR6LXBhcGVyLnBkZgAOACAADwBmAHIAaQB0AHoALQBwAGEAcABlAHIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAEBVc2Vycy9jc3Rhbi9Ecm9wYm94L015IE1hYyAoTWFjQm9vay1Qcm8pL0Rlc2t0b3AvZnJpdHotcGFwZXIucGRmABMAAS8AABUAAgAM//8AAAAIAA0AGgAkAFwAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAAB3g==}} |
|
69 @software{regexploit2021, |
|
70 author = {Ben Caller, Luca Carettoni}, |
|
71 date-added = {2020-11-24 00:00:00 +0000}, |
|
72 date-modified = {2021-05-07 00:00:00 +0000}, |
|
73 keywords = {ReDos static analyser}, |
|
74 month = {May} |
|
75 title = {regexploit} |
|
76 url = {https://github.com/doyensec/regexploit} |
|
77 year = {2021} |
|
78 } |
|
79 |
|
80 @misc{SE16, |
|
81 author = {StackStatus}, |
|
82 date-added = {2019-06-26 11:28:41 +0000}, |
|
83 date-modified = {2019-06-26 16:07:31 +0000}, |
|
84 keywords = {ReDos Attack}, |
|
85 month = {July}, |
|
86 rating = {5}, |
|
87 read = {1}, |
|
88 title = {Stack Overflow Outage Postmortem}, |
|
89 url = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}, |
|
90 year = {2016}, |
|
91 bdsk-url-1 = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}} |
|
92 |
|
93 @article{HosoyaVouillonPierce2005, |
|
94 author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce}, |
|
95 journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)}, |
|
96 number = 1, |
|
97 pages = {46--90}, |
|
98 title = {{R}egular {E}xpression {T}ypes for {XML}}, |
|
99 volume = 27, |
|
100 year = {2005}} |
|
101 |
|
102 @misc{POSIX, |
|
103 note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}}, |
|
104 title = {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition}, |
|
105 year = {2004}} |
|
106 |
|
107 @inproceedings{AusafDyckhoffUrban2016, |
|
108 author = {F.~Ausaf and R.~Dyckhoff and C.~Urban}, |
|
109 booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)}, |
|
110 pages = {69--86}, |
|
111 series = {LNCS}, |
|
112 title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)}, |
|
113 volume = {9807}, |
|
114 year = {2016}} |
|
115 |
|
116 @article{aduAFP16, |
|
117 author = {F.~Ausaf and R.~Dyckhoff and C.~Urban}, |
|
118 issn = {2150-914x}, |
|
119 journal = {Archive of Formal Proofs}, |
|
120 note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development}, |
|
121 title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions}, |
|
122 year = 2016} |
|
123 |
|
124 @techreport{CrashCourse2014, |
|
125 annote = {draft report}, |
|
126 author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen}, |
|
127 institution = {University of Copenhagen}, |
|
128 title = {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular {E}xpressions as {T}ypes}, |
|
129 year = {2014}} |
|
130 |
|
131 @inproceedings{Sulzmann2014, |
|
132 author = {M.~Sulzmann and K.~Lu}, |
|
133 booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)}, |
|
134 pages = {203--220}, |
|
135 series = {LNCS}, |
|
136 title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives}, |
|
137 volume = {8475}, |
|
138 year = {2014}} |
|
139 |
|
140 @inproceedings{Sulzmann2014b, |
|
141 author = {M.~Sulzmann and P.~van Steenhoven}, |
|
142 booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)}, |
|
143 pages = {174--191}, |
|
144 series = {LNCS}, |
|
145 title = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular {E}xpression {S}ubmatching}, |
|
146 volume = {8409}, |
|
147 year = {2014}} |
|
148 |
|
149 @book{Pierce2015, |
|
150 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}, |
|
151 note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}}, |
|
152 publisher = {Electronic textbook}, |
|
153 title = {{S}oftware {F}oundations}, |
|
154 year = {2015}} |
|
155 |
|
156 @misc{Kuklewicz, |
|
157 author = {C.~Kuklewicz}, |
|
158 howpublished = {\url{https://wiki.haskell.org/Regex_Posix}}, |
|
159 title = {{R}egex {P}osix}} |
|
160 |
|
161 @article{Vansummeren2006, |
|
162 author = {S.~Vansummeren}, |
|
163 journal = {ACM Transactions on Programming Languages and Systems}, |
|
164 number = {3}, |
|
165 pages = {389--428}, |
|
166 title = {{T}ype {I}nference for {U}nique {P}attern {M}atching}, |
|
167 volume = {28}, |
|
168 year = {2006}} |
|
169 |
|
170 @inproceedings{Asperti12, |
|
171 author = {A.~Asperti}, |
|
172 booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)}, |
|
173 pages = {283--298}, |
|
174 series = {LNCS}, |
|
175 title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence}, |
|
176 volume = {7406}, |
|
177 year = {2012}} |
|
178 |
|
179 @inproceedings{Frisch2004, |
|
180 author = {A.~Frisch and L.~Cardelli}, |
|
181 booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)}, |
|
182 pages = {618--629}, |
|
183 series = {LNCS}, |
|
184 title = {{G}reedy {R}egular {E}xpression {M}atching}, |
|
185 volume = {3142}, |
|
186 year = {2004}} |
|
187 |
|
188 @article{Antimirov95, |
|
189 author = {V.~Antimirov}, |
|
190 journal = {Theoretical Computer Science}, |
|
191 pages = {291--319}, |
|
192 title = {{P}artial {D}erivatives of {R}egular {E}xpressions and {F}inite {A}utomata {C}onstructions}, |
|
193 volume = {155}, |
|
194 year = {1995}} |
|
195 |
|
196 @inproceedings{Nipkow98, |
|
197 author = {T.~Nipkow}, |
|
198 booktitle = {Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)}, |
|
199 pages = {1--15}, |
|
200 series = {LNCS}, |
|
201 title = {{V}erified {L}exical {A}nalysis}, |
|
202 volume = 1479, |
|
203 year = 1998} |
|
204 |
|
205 @article{Brzozowski1964, |
|
206 author = {J.~A.~Brzozowski}, |
|
207 journal = {Journal of the {ACM}}, |
|
208 number = {4}, |
|
209 pages = {481--494}, |
|
210 title = {{D}erivatives of {R}egular {E}xpressions}, |
|
211 volume = {11}, |
|
212 year = {1964}} |
|
213 |
|
214 @article{Leroy2009, |
|
215 author = {X.~Leroy}, |
|
216 journal = {Communications of the ACM}, |
|
217 number = 7, |
|
218 pages = {107--115}, |
|
219 title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler}, |
|
220 volume = 52, |
|
221 year = 2009} |
|
222 |
|
223 @inproceedings{Paulson2015, |
|
224 author = {L.~C.~Paulson}, |
|
225 booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)}, |
|
226 pages = {231--245}, |
|
227 series = {LNAI}, |
|
228 title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets}, |
|
229 volume = {9195}, |
|
230 year = {2015}} |
|
231 |
|
232 @article{Wu2014, |
|
233 author = {C.~Wu and X.~Zhang and C.~Urban}, |
|
234 journal = {Journal of Automatic Reasoning}, |
|
235 number = {4}, |
|
236 pages = {451--480}, |
|
237 title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions}, |
|
238 volume = {52}, |
|
239 year = {2014}} |
|
240 |
|
241 @inproceedings{Regehr2011, |
|
242 author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr}, |
|
243 booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)}, |
|
244 pages = {283--294}, |
|
245 title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers}, |
|
246 year = {2011}} |
|
247 |
|
248 @article{Norrish2014, |
|
249 author = {A.~Barthwal and M.~Norrish}, |
|
250 journal = {Journal of Computer and System Sciences}, |
|
251 number = {2}, |
|
252 pages = {346--362}, |
|
253 title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}}, |
|
254 volume = {80}, |
|
255 year = {2014}} |
|
256 |
|
257 @article{Thompson1968, |
|
258 author = {K.~Thompson}, |
|
259 issue_date = {June 1968}, |
|
260 journal = {Communications of the ACM}, |
|
261 number = {6}, |
|
262 pages = {419--422}, |
|
263 title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm}, |
|
264 volume = {11}, |
|
265 year = {1968}} |
|
266 |
|
267 @article{Owens2009, |
|
268 author = {S.~Owens and J.~H.~Reppy and A.~Turon}, |
|
269 journal = {Journal of Functinal Programming}, |
|
270 number = {2}, |
|
271 pages = {173--190}, |
|
272 title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined}, |
|
273 volume = {19}, |
|
274 year = {2009}} |
|
275 |
|
276 @inproceedings{Sulzmann2015, |
|
277 author = {M.~Sulzmann and P.~Thiemann}, |
|
278 booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory and Applications (LATA)}, |
|
279 pages = {275--286}, |
|
280 series = {LNCS}, |
|
281 title = {{D}erivatives for {R}egular {S}huffle {E}xpressions}, |
|
282 volume = {8977}, |
|
283 year = {2015}} |
|
284 |
|
285 @inproceedings{Chen2012, |
|
286 author = {H.~Chen and S.~Yu}, |
|
287 booktitle = {Proc.~in the International Workshop on Theoretical Computer Science (WTCS)}, |
|
288 pages = {343--356}, |
|
289 series = {LNCS}, |
|
290 title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication}, |
|
291 volume = {7160}, |
|
292 year = {2012}} |
|
293 |
|
294 @article{Krauss2011, |
|
295 author = {A.~Krauss and T.~Nipkow}, |
|
296 journal = {Journal of Automated Reasoning}, |
|
297 pages = {95--106}, |
|
298 title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra}, |
|
299 volume = 49, |
|
300 year = 2012} |
|
301 |
|
302 @inproceedings{Traytel2015, |
|
303 author = {D.~Traytel}, |
|
304 booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)}, |
|
305 pages = {487--503}, |
|
306 series = {LIPIcs}, |
|
307 title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}}, |
|
308 volume = {41}, |
|
309 year = {2015}} |
|
310 |
|
311 @inproceedings{Traytel2013, |
|
312 author = {D.~Traytel and T.~Nipkow}, |
|
313 booktitle = {Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)}, |
|
314 pages = {3-12}, |
|
315 title = {{A} {V}erified {D}ecision {P}rocedure for {MSO} on {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions}, |
|
316 year = 2013} |
|
317 |
|
318 @inproceedings{Coquand2012, |
|
319 author = {T.~Coquand and V.~Siles}, |
|
320 booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)}, |
|
321 pages = {119--134}, |
|
322 series = {LNCS}, |
|
323 title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory}, |
|
324 volume = {7086}, |
|
325 year = {2011}} |
|
326 |
|
327 @inproceedings{Almeidaetal10, |
|
328 author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa}, |
|
329 booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)}, |
|
330 pages = {59-68}, |
|
331 series = {LNCS}, |
|
332 title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq}, |
|
333 volume = {6482}, |
|
334 year = {2010}} |
|
335 |
|
336 @article{Owens2008, |
|
337 author = {S.~Owens and K.~Slind}, |
|
338 journal = {Higher-Order and Symbolic Computation}, |
|
339 number = {4}, |
|
340 pages = {377--409}, |
|
341 title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic}, |
|
342 volume = {21}, |
|
343 year = {2008}} |
|
344 |
|
345 @article{Owens2, |
|
346 author = {S.~Owens and K.~Slind}, |
|
347 bibsource = {dblp computer science bibliography, http://dblp.org}, |
|
348 biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08}, |
|
349 doi = {10.1007/s10990-008-9038-0}, |
|
350 journal = {Higher-Order and Symbolic Computation}, |
|
351 number = {4}, |
|
352 pages = {377--409}, |
|
353 timestamp = {Wed, 16 Dec 2009 13:51:02 +0100}, |
|
354 title = {Adapting functional programs to higher order logic}, |
|
355 url = {http://dx.doi.org/10.1007/s10990-008-9038-0}, |
|
356 volume = {21}, |
|
357 year = {2008}, |
|
358 bdsk-url-1 = {http://dx.doi.org/10.1007/s10990-008-9038-0}} |
|
359 |
|
360 @misc{PCRE, |
|
361 title = {{PCRE - Perl Compatible Regular Expressions}}, |
|
362 url = {http://www.pcre.org}, |
|
363 bdsk-url-1 = {http://www.pcre.org}} |
|
364 |
|
365 @inproceedings{OkuiSuzuki2010, |
|
366 author = {S.~Okui and T.~Suzuki}, |
|
367 booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)}, |
|
368 pages = {231--240}, |
|
369 series = {LNCS}, |
|
370 title = {{D}isambiguation in {R}egular {E}xpression {M}atching via {P}osition {A}utomata with {A}ugmented {T}ransitions}, |
|
371 volume = {6482}, |
|
372 year = {2010}} |
|
373 |
|
374 @techreport{OkuiSuzukiTech, |
|
375 author = {S.~Okui and T.~Suzuki}, |
|
376 institution = {University of Aizu}, |
|
377 title = {{D}isambiguation in {R}egular {E}xpression {M}atching via {P}osition {A}utomata with {A}ugmented {T}ransitions}, |
|
378 year = {2013}} |
|
379 |
|
380 @inproceedings{Davis18, |
|
381 author = {J.~C.~Davis and C.~.A.~Coghlan and F.~Servant and D.~Lee}, |
|
382 booktitle = {Proc.~of the 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)}, |
|
383 numpages = {11}, |
|
384 pages = {246--256}, |
|
385 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}, |
|
386 year = {2018}} |