%% This BibTeX bibliography file was created using BibDesk.
%% https://bibdesk.sourceforge.io/
%% Created for CS TAN at 2019-08-18 19:00:13 +0100
%% Saved with string encoding Unicode (UTF-8)
@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{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 = {YnBsaXN0MDDUAQIDBAUGJCVYJHZlcnNpb25YJG9iamVjdHNZJGFyY2hpdmVyVCR0b3ASAAGGoKgHCBMUFRYaIVUkbnVsbNMJCgsMDxJXTlMua2V5c1pOUy5vYmplY3RzViRjbGFzc6INDoACgAOiEBGABIAFgAdccmVsYXRpdmVQYXRoWWFsaWFzRGF0YV8QGC4uLy4uLy4uL2ZyaXR6LXBhcGVyLnBkZtIXCxgZV05TLmRhdGFPEQFGAAAAAAFGAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8PZnJpdHotcGFwZXIucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAADAAEAAAogY3UAAAAAAAAAAAAAAAAAB0Rlc2t0b3AAAAIAJS86VXNlcnM6Y3N0YW46RGVza3RvcDpmcml0ei1wYXBlci5wZGYAAA4AIAAPAGYAcgBpAHQAegAtAHAAYQBwAGUAcgAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIAI1VzZXJzL2NzdGFuL0Rlc2t0b3AvZnJpdHotcGFwZXIucGRmAAATAAEvAAAVAAIADP//AACABtIbHB0eWiRjbGFzc25hbWVYJGNsYXNzZXNdTlNNdXRhYmxlRGF0YaMdHyBWTlNEYXRhWE5TT2JqZWN00hscIiNcTlNEaWN0aW9uYXJ5oiIgXxAPTlNLZXllZEFyY2hpdmVy0SYnVHJvb3SAAQAIABEAGgAjAC0AMgA3AEAARgBNAFUAYABnAGoAbABuAHEAcwB1AHcAhACOAKkArgC2AgACAgIHAhICGwIpAi0CNAI9AkICTwJSAmQCZwJsAAAAAAAAAgEAAAAAAAAAKAAAAAAAAAAAAAAAAAAAAm4=}}
@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}}