%% This BibTeX bibliography file was created using BibDesk.

%% https://bibdesk.sourceforge.io/

%% Saved with string encoding Unicode (UTF-8) 

@article{Rathnayake2014StaticAF,

@inproceedings{Weideman2017Static,

@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,

@article{alfred2014algorithms,

@article{CAMPEANU2009Intersect,

@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},

@misc{KuklewiczHaskell,

	author = {Kuklewicz},

	keywords = {Buggy C POSIX Lexing Libraries},

	url = {https://wiki.haskell.org/Regex_Posix},

@misc{regex101,

	author = {Firas Dib},

	url = {https://regex101.com/},

@misc{atomEditor,

	title = {Atom Editor},

	year = {2022},

@techreport{grathwohl2014crash,

@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}}