%% This BibTeX bibliography file was created using BibDesk.+ −
%% https://bibdesk.sourceforge.io/+ −
+ −
%% Created for CS TAN at 2022-03-16 16:38:47 +0000 + −
+ −
+ −
%% Saved with string encoding Unicode (UTF-8) + −
+ −
@article{Rathnayake2014StaticAF,+ −
title={Static Analysis for Regular Expression Exponential Runtime via Substructural Logics},+ −
author={Asiri Rathnayake and Hayo Thielecke},+ −
journal={ArXiv,+ −
year={2014},+ −
volume={abs/1405.7058}+ −
}+ −
+ −
@inproceedings{RibeiroAgda2017,+ −
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.},+ −
address = {New York, NY, USA},+ −
articleno = {4},+ −
author = {Ribeiro, Rodrigo and Bois, Andr\'{e} Du},+ −
booktitle = {Proceedings of the 21st Brazilian Symposium on Programming Languages},+ −
date-modified = {2022-03-16 16:38:47 +0000},+ −
doi = {10.1145/3125374.3125381},+ −
isbn = {9781450353892},+ −
keywords = {Certified algorithms, regular expressions, dependent types, bit-codes},+ −
location = {Fortaleza, CE, Brazil},+ −
numpages = {8},+ −
publisher = {Association for Computing Machinery},+ −
series = {SBLP 2017},+ −
title = {Certified Bit-Coded Regular Expression Parsing},+ −
url = {https://doi.org/10.1145/3125374.3125381},+ −
year = {2017},+ −
bdsk-url-1 = {https://doi.org/10.1145/3125374.3125381}}+ −
+ −
@article{Thompson_1968,+ −
author = {Ken Thompson},+ −
date-added = {2022-02-23 13:44:42 +0000},+ −
date-modified = {2022-02-23 13:44:42 +0000},+ −
doi = {10.1145/363347.363387},+ −
journal = {Communications of the {ACM}},+ −
month = {jun},+ −
number = {6},+ −
pages = {419--422},+ −
publisher = {Association for Computing Machinery ({ACM})},+ −
title = {Programming Techniques: Regular expression search algorithm},+ −
url = {https://doi.org/10.1145%2F363347.363387},+ −
volume = {11},+ −
year = 1968,+ −
bdsk-url-1 = {https://doi.org/10.1145%2F363347.363387},+ −
bdsk-url-2 = {https://doi.org/10.1145/363347.363387}}+ −
+ −
@article{17Bir,+ −
author = {Asiri Rathnayake and Hayo Thielecke},+ −
date-added = {2019-08-18 17:57:30 +0000},+ −
date-modified = {2019-08-18 18:00:13 +0000},+ −
journal = {arXiv:1405.7058},+ −
title = {Static Analysis for Regular Expression Exponential Runtime via Substructural Logics},+ −
year = {2017}}+ −
@article{campeanu2003formal,+ −
title={A formal study of practical regular expressions},+ −
author={C{\^a}mpeanu, Cezar and Salomaa, Kai and Yu, Sheng},+ −
journal={International Journal of Foundations of Computer Science},+ −
volume={14},+ −
number={06},+ −
pages={1007--1018},+ −
year={2003},+ −
publisher={World Scientific}+ −
}+ −
+ −
@article{alfred2014algorithms,+ −
title={Algorithms for finding patterns in strings},+ −
author={Alfred, V},+ −
journal={Algorithms and Complexity},+ −
volume={1},+ −
pages={255},+ −
year={2014},+ −
publisher={Elsevier}+ −
}+ −
+ −
+ −
@article{CAMPEANU2009Intersect,+ −
title = {On the intersection of regex languages with regular languages},+ −
journal = {Theoretical Computer Science},+ −
volume = {410},+ −
number = {24},+ −
pages = {2336-2344},+ −
year = {2009},+ −
note = {Formal Languages and Applications: A Collection of Papers in Honor of Sheng Yu},+ −
issn = {0304-3975},+ −
doi = {https://doi.org/10.1016/j.tcs.2009.02.022},+ −
url = {https://www.sciencedirect.com/science/article/pii/S0304397509001789},+ −
author = {Cezar Câmpeanu and Nicolae Santean},+ −
keywords = {Extended regular expression, Regex automata system, Regex},+ −
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âmpeanu, Salomaa and Yu [C. Câ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.}+ −
}+ −
+ −
+ −
@article{nielson11bcre,+ −
author = {Lasse Nielsen, Fritz Henglein},+ −
date-added = {2019-07-03 21:09:39 +0000},+ −
date-modified = {2019-07-03 21:17:33 +0000},+ −
journal = {LATA},+ −
title = {Bit-coded Regular Expression Parsing},+ −
year = {2011},+ −
bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxA1Li4vLi4vLi4vTXkgTWFjIChNYWNCb29rLVBybykvRGVza3RvcC9mcml0ei1wYXBlci5wZGZPEQF+AAAAAAF+AAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8PZnJpdHotcGFwZXIucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAMAAAogY3UAAAAAAAAAAAAAAAAAB0Rlc2t0b3AAAAIAQi86VXNlcnM6Y3N0YW46RHJvcGJveDpNeSBNYWMgKE1hY0Jvb2stUHJvKTpEZXNrdG9wOmZyaXR6LXBhcGVyLnBkZgAOACAADwBmAHIAaQB0AHoALQBwAGEAcABlAHIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAEBVc2Vycy9jc3Rhbi9Ecm9wYm94L015IE1hYyAoTWFjQm9vay1Qcm8pL0Rlc2t0b3AvZnJpdHotcGFwZXIucGRmABMAAS8AABUAAgAM//8AAAAIAA0AGgAkAFwAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAAB3g==}}+ −
@software{regexploit2021,+ −
author = {Ben Caller, Luca Carettoni},+ −
date-added = {2020-11-24 00:00:00 +0000},+ −
date-modified = {2021-05-07 00:00:00 +0000},+ −
keywords = {ReDos static analyser},+ −
month = {May}+ −
title = {regexploit}+ −
url = {https://github.com/doyensec/regexploit}+ −
year = {2021}+ −
}+ −
+ −
@misc{KuklewiczHaskell,+ −
title = {Regex Posix},+ −
author = {Kuklewicz},+ −
keywords = {Buggy C POSIX Lexing Libraries},+ −
url = {https://wiki.haskell.org/Regex_Posix},+ −
year = {2017}+ −
}+ −
+ −
+ −
@techreport{grathwohl2014crash,+ −
title={A Crash-Course in Regular Expression Parsing and Regular Expressions as Types},+ −
author={Grathwohl, Niels Bj{\o}rn Bugge and Henglein, Fritz and Rasmussen, Ulrik Terp},+ −
year={2014},+ −
institution={Technical report, University of Copenhagen}+ −
}+ −
+ −
@misc{SE16,+ −
author = {StackStatus},+ −
date-added = {2019-06-26 11:28:41 +0000},+ −
date-modified = {2019-06-26 16:07:31 +0000},+ −
keywords = {ReDos Attack},+ −
month = {July},+ −
rating = {5},+ −
read = {1},+ −
title = {Stack Overflow Outage Postmortem},+ −
url = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016},+ −
year = {2016},+ −
bdsk-url-1 = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}}+ −
+ −
@article{HosoyaVouillonPierce2005,+ −
author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce},+ −
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},+ −
number = 1,+ −
pages = {46--90},+ −
title = {{R}egular {E}xpression {T}ypes for {XML}},+ −
volume = 27,+ −
year = {2005}}+ −
+ −
@misc{POSIX,+ −
note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}},+ −
title = {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition},+ −
year = {2004}}+ −
+ −
@inproceedings{AusafDyckhoffUrban2016,+ −
author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},+ −
booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)},+ −
pages = {69--86},+ −
series = {LNCS},+ −
title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)},+ −
volume = {9807},+ −
year = {2016}}+ −
+ −
@article{aduAFP16,+ −
author = {F.~Ausaf and R.~Dyckhoff and C.~Urban},+ −
issn = {2150-914x},+ −
journal = {Archive of Formal Proofs},+ −
note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development},+ −
title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions},+ −
year = 2016}+ −
+ −
@techreport{CrashCourse2014,+ −
annote = {draft report},+ −
author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen},+ −
institution = {University of Copenhagen},+ −
title = {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular {E}xpressions as {T}ypes},+ −
year = {2014}}+ −
+ −
@inproceedings{Sulzmann2014,+ −
author = {M.~Sulzmann and K.~Lu},+ −
booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)},+ −
pages = {203--220},+ −
series = {LNCS},+ −
title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives},+ −
volume = {8475},+ −
year = {2014}}+ −
+ −
@inproceedings{Sulzmann2014b,+ −
author = {M.~Sulzmann and P.~van Steenhoven},+ −
booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)},+ −
pages = {174--191},+ −
series = {LNCS},+ −
title = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular {E}xpression {S}ubmatching},+ −
volume = {8409},+ −
year = {2014}}+ −
+ −
@book{Pierce2015,+ −
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},+ −
note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}},+ −
publisher = {Electronic textbook},+ −
title = {{S}oftware {F}oundations},+ −
year = {2015}}+ −
+ −
@misc{Kuklewicz,+ −
author = {C.~Kuklewicz},+ −
howpublished = {\url{https://wiki.haskell.org/Regex_Posix}},+ −
title = {{R}egex {P}osix}}+ −
+ −
@article{Vansummeren2006,+ −
author = {S.~Vansummeren},+ −
journal = {ACM Transactions on Programming Languages and Systems},+ −
number = {3},+ −
pages = {389--428},+ −
title = {{T}ype {I}nference for {U}nique {P}attern {M}atching},+ −
volume = {28},+ −
year = {2006}}+ −
+ −
@inproceedings{Asperti12,+ −
author = {A.~Asperti},+ −
booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)},+ −
pages = {283--298},+ −
series = {LNCS},+ −
title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},+ −
volume = {7406},+ −
year = {2012}}+ −
+ −
@inproceedings{Frisch2004,+ −
author = {A.~Frisch and L.~Cardelli},+ −
booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)},+ −
pages = {618--629},+ −
series = {LNCS},+ −
title = {{G}reedy {R}egular {E}xpression {M}atching},+ −
volume = {3142},+ −
year = {2004}}+ −
+ −
@article{Antimirov95,+ −
author = {V.~Antimirov},+ −
journal = {Theoretical Computer Science},+ −
pages = {291--319},+ −
title = {{P}artial {D}erivatives of {R}egular {E}xpressions and {F}inite {A}utomata {C}onstructions},+ −
volume = {155},+ −
year = {1995}}+ −
+ −
@inproceedings{Nipkow98,+ −
author = {T.~Nipkow},+ −
booktitle = {Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)},+ −
pages = {1--15},+ −
series = {LNCS},+ −
title = {{V}erified {L}exical {A}nalysis},+ −
volume = 1479,+ −
year = 1998}+ −
+ −
@article{Brzozowski1964,+ −
author = {J.~A.~Brzozowski},+ −
journal = {Journal of the {ACM}},+ −
number = {4},+ −
pages = {481--494},+ −
title = {{D}erivatives of {R}egular {E}xpressions},+ −
volume = {11},+ −
year = {1964}}+ −
+ −
@article{Leroy2009,+ −
author = {X.~Leroy},+ −
journal = {Communications of the ACM},+ −
number = 7,+ −
pages = {107--115},+ −
title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler},+ −
volume = 52,+ −
year = 2009}+ −
+ −
@inproceedings{Paulson2015,+ −
author = {L.~C.~Paulson},+ −
booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)},+ −
pages = {231--245},+ −
series = {LNAI},+ −
title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets},+ −
volume = {9195},+ −
year = {2015}}+ −
+ −
@article{Wu2014,+ −
author = {C.~Wu and X.~Zhang and C.~Urban},+ −
journal = {Journal of Automatic Reasoning},+ −
number = {4},+ −
pages = {451--480},+ −
title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},+ −
volume = {52},+ −
year = {2014}}+ −
+ −
@inproceedings{Regehr2011,+ −
author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr},+ −
booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)},+ −
pages = {283--294},+ −
title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers},+ −
year = {2011}}+ −
+ −
@article{Norrish2014,+ −
author = {A.~Barthwal and M.~Norrish},+ −
journal = {Journal of Computer and System Sciences},+ −
number = {2},+ −
pages = {346--362},+ −
title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}},+ −
volume = {80},+ −
year = {2014}}+ −
+ −
@article{Thompson1968,+ −
author = {K.~Thompson},+ −
issue_date = {June 1968},+ −
journal = {Communications of the ACM},+ −
number = {6},+ −
pages = {419--422},+ −
title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm},+ −
volume = {11},+ −
year = {1968}}+ −
+ −
@article{Owens2009,+ −
author = {S.~Owens and J.~H.~Reppy and A.~Turon},+ −
journal = {Journal of Functinal Programming},+ −
number = {2},+ −
pages = {173--190},+ −
title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},+ −
volume = {19},+ −
year = {2009}}+ −
+ −
@inproceedings{Sulzmann2015,+ −
author = {M.~Sulzmann and P.~Thiemann},+ −
booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory and Applications (LATA)},+ −
pages = {275--286},+ −
series = {LNCS},+ −
title = {{D}erivatives for {R}egular {S}huffle {E}xpressions},+ −
volume = {8977},+ −
year = {2015}}+ −
+ −
@inproceedings{Chen2012,+ −
author = {H.~Chen and S.~Yu},+ −
booktitle = {Proc.~in the International Workshop on Theoretical Computer Science (WTCS)},+ −
pages = {343--356},+ −
series = {LNCS},+ −
title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication},+ −
volume = {7160},+ −
year = {2012}}+ −
+ −
@article{Krauss2011,+ −
author = {A.~Krauss and T.~Nipkow},+ −
journal = {Journal of Automated Reasoning},+ −
pages = {95--106},+ −
title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},+ −
volume = 49,+ −
year = 2012}+ −
+ −
@inproceedings{Traytel2015,+ −
author = {D.~Traytel},+ −
booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)},+ −
pages = {487--503},+ −
series = {LIPIcs},+ −
title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}},+ −
volume = {41},+ −
year = {2015}}+ −
+ −
@inproceedings{Traytel2013,+ −
author = {D.~Traytel and T.~Nipkow},+ −
booktitle = {Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)},+ −
pages = {3-12},+ −
title = {{A} {V}erified {D}ecision {P}rocedure for {MSO} on {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions},+ −
year = 2013}+ −
+ −
@inproceedings{Coquand2012,+ −
author = {T.~Coquand and V.~Siles},+ −
booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)},+ −
pages = {119--134},+ −
series = {LNCS},+ −
title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},+ −
volume = {7086},+ −
year = {2011}}+ −
+ −
@inproceedings{Almeidaetal10,+ −
author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa},+ −
booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)},+ −
pages = {59-68},+ −
series = {LNCS},+ −
title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq},+ −
volume = {6482},+ −
year = {2010}}+ −
+ −
@article{Owens2008,+ −
author = {S.~Owens and K.~Slind},+ −
journal = {Higher-Order and Symbolic Computation},+ −
number = {4},+ −
pages = {377--409},+ −
title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},+ −
volume = {21},+ −
year = {2008}}+ −
+ −
@article{Owens2,+ −
author = {S.~Owens and K.~Slind},+ −
bibsource = {dblp computer science bibliography, http://dblp.org},+ −
biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08},+ −
doi = {10.1007/s10990-008-9038-0},+ −
journal = {Higher-Order and Symbolic Computation},+ −
number = {4},+ −
pages = {377--409},+ −
timestamp = {Wed, 16 Dec 2009 13:51:02 +0100},+ −
title = {Adapting functional programs to higher order logic},+ −
url = {http://dx.doi.org/10.1007/s10990-008-9038-0},+ −
volume = {21},+ −
year = {2008},+ −
bdsk-url-1 = {http://dx.doi.org/10.1007/s10990-008-9038-0}}+ −
+ −
@misc{PCRE,+ −
title = {{PCRE - Perl Compatible Regular Expressions}},+ −
url = {http://www.pcre.org},+ −
bdsk-url-1 = {http://www.pcre.org}}+ −
+ −
@inproceedings{OkuiSuzuki2010,+ −
author = {S.~Okui and T.~Suzuki},+ −
booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)},+ −
pages = {231--240},+ −
series = {LNCS},+ −
title = {{D}isambiguation in {R}egular {E}xpression {M}atching via {P}osition {A}utomata with {A}ugmented {T}ransitions},+ −
volume = {6482},+ −
year = {2010}}+ −
+ −
@techreport{OkuiSuzukiTech,+ −
author = {S.~Okui and T.~Suzuki},+ −
institution = {University of Aizu},+ −
title = {{D}isambiguation in {R}egular {E}xpression {M}atching via {P}osition {A}utomata with {A}ugmented {T}ransitions},+ −
year = {2013}}+ −
+ −
@inproceedings{Davis18,+ −
author = {J.~C.~Davis and C.~.A.~Coghlan and F.~Servant and D.~Lee},+ −
booktitle = {Proc.~of the 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)},+ −
numpages = {11},+ −
pages = {246--256},+ −
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},+ −
year = {2018}}+ −