# HG changeset patch # User Chengsong # Date 1561561618 -3600 # Node ID feffec3af1a1d85004fafefbc5ad915f0fcf5e6c # Parent e70f18e77e56cbe22012961700626b4c8f94fc7e now correct diff -r e70f18e77e56 -r feffec3af1a1 ecp/.DS_Store Binary file ecp/.DS_Store has changed diff -r e70f18e77e56 -r feffec3af1a1 ecp/data.sty --- a/ecp/data.sty Wed Jun 26 12:44:08 2019 +0100 +++ b/ecp/data.sty Wed Jun 26 16:06:58 2019 +0100 @@ -1,6 +1,26 @@ % The data files, written on the first run. - +%% example a?{n} a{n} +\begin{filecontents}{re-python.data} +1 0.029 +5 0.029 +10 0.029 +15 0.032 +16 0.042 +17 0.042 +18 0.055 +19 0.084 +20 0.136 +21 0.248 +22 0.464 +23 0.899 +24 1.773 +25 3.505 +26 6.993 +27 14.503 +28 29.307 +#29 58.886 +\end{filecontents} \begin{filecontents}{re-python2.data} @@ -21,7 +41,37 @@ 28 26.69 \end{filecontents} - +%% example a?{n} a{n} +\begin{filecontents}{re-ruby.data} +1 0.00006 +#2 0.00003 +#3 0.00001 +#4 0.00001 +5 0.00001 +#6 0.00002 +#7 0.00002 +#8 0.00004 +#9 0.00007 +10 0.00013 +#11 0.00026 +#12 0.00055 +#13 0.00106 +#14 0.00196 +15 0.00378 +16 0.00764 +17 0.01606 +18 0.03094 +19 0.06508 +20 0.12420 +21 0.25393 +22 0.51449 +23 1.02174 +24 2.05998 +25 4.22514 +26 8.42479 +27 16.88678 +28 34.79653 +\end{filecontents} % JavaScript, example (a*)*b \begin{filecontents}{re-js.data} diff -r e70f18e77e56 -r feffec3af1a1 ecp/ecoop_paper.tex --- a/ecp/ecoop_paper.tex Wed Jun 26 12:44:08 2019 +0100 +++ b/ecp/ecoop_paper.tex Wed Jun 26 16:06:58 2019 +0100 @@ -11,7 +11,7 @@ %\usepackage{pmboxdraw} \title{POSIX Regular Expression Matching and Lexing} -\author[1]{Annonymous} +\author[1]{Chengsong Tan \\ King's College London\\chengsong.tan@kcl.ac.uk} \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% \newcommand{\ZERO}{\mbox{\bf 0}} @@ -160,7 +160,7 @@ This exponential blowup sometimes causes real pain in ``real life'': for example one evil regular expression brought on 20 July 2016 the -webpage \href{http://stackexchange.com}{Stack Exchange} to its knees. +webpage \href{http://stackexchange.com}{Stack Exchange} to its knees\cite{SE16}. In this instance, a regular expression intended to just trim white spaces from the beginning and the end of a line actually consumed massive amounts of CPU-resources and because of this the web servers diff -r e70f18e77e56 -r feffec3af1a1 ecp/root.bib --- a/ecp/root.bib Wed Jun 26 12:44:08 2019 +0100 +++ b/ecp/root.bib Wed Jun 26 16:06:58 2019 +0100 @@ -1,350 +1,318 @@ -@article{HosoyaVouillonPierce2005, - author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce}, - title = {{R}egular {E}xpression {T}ypes for {XML}}, - journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)}, - year = {2005}, - volume = 27, - number = 1, - pages = {46--90} -} - - -@Misc{POSIX, - title = {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition}, - year = {2004}, - note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}} -} - +%% This BibTeX bibliography file was created using BibDesk. +%% https://bibdesk.sourceforge.io/ -@InProceedings{AusafDyckhoffUrban2016, - author = {F.~Ausaf and R.~Dyckhoff and C.~Urban}, - title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)}, - year = {2016}, - booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)}, - volume = {9807}, - series = {LNCS}, - pages = {69--86} -} - -@article{aduAFP16, - author = {F.~Ausaf and R.~Dyckhoff and C.~Urban}, - title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions}, - journal = {Archive of Formal Proofs}, - year = 2016, - note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development}, - ISSN = {2150-914x} -} +%% Created for CS TAN at 2019-06-26 12:42:11 +0100 -@TechReport{CrashCourse2014, - author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen}, - title = {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular - {E}xpressions as {T}ypes}, - institution = {University of Copenhagen}, - year = {2014}, - annote = {draft report} -} - -@inproceedings{Sulzmann2014, - author = {M.~Sulzmann and K.~Lu}, - title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives}, - booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)}, - pages = {203--220}, - year = {2014}, - volume = {8475}, - series = {LNCS} -} - -@inproceedings{Sulzmann2014b, - author = {M.~Sulzmann and P.~van Steenhoven}, - title = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular - {E}xpression {S}ubmatching}, - booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)}, - pages = {174--191}, - year = {2014}, - volume = {8409}, - series = {LNCS} -} - -@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}, - title = {{S}oftware {F}oundations}, - year = {2015}, - publisher = {Electronic textbook}, - note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}} -} - -@Misc{Kuklewicz, - author = {C.~Kuklewicz}, - title = {{R}egex {P}osix}, - howpublished = "\url{https://wiki.haskell.org/Regex_Posix}" -} - -@article{Vansummeren2006, - author = {S.~Vansummeren}, - title = {{T}ype {I}nference for {U}nique {P}attern {M}atching}, - year = {2006}, - journal = {ACM Transactions on Programming Languages and Systems}, - volume = {28}, - number = {3}, - pages = {389--428} -} - -@InProceedings{Asperti12, - author = {A.~Asperti}, - title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence}, - booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)}, - pages = {283--298}, - year = {2012}, - volume = {7406}, - series = {LNCS} -} - -@inproceedings{Frisch2004, - author = {A.~Frisch and L.~Cardelli}, - title = {{G}reedy {R}egular {E}xpression {M}atching}, - booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)}, - pages = {618--629}, - year = {2004}, - volume = {3142}, - series = {LNCS} -} - -@ARTICLE{Antimirov95, - author = {V.~Antimirov}, - title = {{P}artial {D}erivatives of {R}egular {E}xpressions and - {F}inite {A}utomata {C}onstructions}, - journal = {Theoretical Computer Science}, - year = {1995}, - volume = {155}, - pages = {291--319} -} - -@inproceedings{Nipkow98, - author={T.~Nipkow}, - title={{V}erified {L}exical {A}nalysis}, - booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)}, - series={LNCS}, - volume=1479, - pages={1--15}, - year=1998 -} - -@article{Brzozowski1964, - author = {J.~A.~Brzozowski}, - title = {{D}erivatives of {R}egular {E}xpressions}, - journal = {Journal of the {ACM}}, - volume = {11}, - number = {4}, - pages = {481--494}, - year = {1964} -} - -@article{Leroy2009, - author = {X.~Leroy}, - title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler}, - journal = {Communications of the ACM}, - year = 2009, - volume = 52, - number = 7, - pages = {107--115} -} - -@InProceedings{Paulson2015, - author = {L.~C.~Paulson}, - title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets}, - booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)}, - pages = {231--245}, - year = {2015}, - volume = {9195}, - series = {LNAI} -} - -@Article{Wu2014, - author = {C.~Wu and X.~Zhang and C.~Urban}, - title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions}, - journal = {Journal of Automatic Reasoning}, - year = {2014}, - volume = {52}, - number = {4}, - pages = {451--480} -} - -@InProceedings{Regehr2011, - author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr}, - title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers}, - pages = {283--294}, - year = {2011}, - booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and - Implementation (PLDI)} -} - -@Article{Norrish2014, - author = {A.~Barthwal and M.~Norrish}, - title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}}, - journal = {Journal of Computer and System Sciences}, - year = {2014}, - volume = {80}, - number = {2}, - pages = {346--362} -} - -@Article{Thompson1968, - author = {K.~Thompson}, - title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm}, - journal = {Communications of the ACM}, - issue_date = {June 1968}, - volume = {11}, - number = {6}, - year = {1968}, - pages = {419--422} -} - -@article{Owens2009, - author = {S.~Owens and J.~H.~Reppy and A.~Turon}, - title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined}, - journal = {Journal of Functinal Programming}, - volume = {19}, - number = {2}, - pages = {173--190}, - year = {2009} -} - -@inproceedings{Sulzmann2015, - author = {M.~Sulzmann and P.~Thiemann}, - title = {{D}erivatives for {R}egular {S}huffle {E}xpressions}, - booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory - and Applications (LATA)}, - pages = {275--286}, - year = {2015}, - volume = {8977}, - series = {LNCS} -} - -@inproceedings{Chen2012, - author = {H.~Chen and S.~Yu}, - title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication}, - booktitle = {Proc.~in the International Workshop on Theoretical - Computer Science (WTCS)}, - pages = {343--356}, - year = {2012}, - volume = {7160}, - series = {LNCS} -} - -@article{Krauss2011, - author={A.~Krauss and T.~Nipkow}, - title={{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra}, - journal={Journal of Automated Reasoning}, - volume=49, - pages={95--106}, - year=2012 -} - -@InProceedings{Traytel2015, - author = {D.~Traytel}, - title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}}, - booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)}, - pages = {487--503}, - series = {LIPIcs}, - year = {2015}, - volume = {41} -} - -@inproceedings{Traytel2013, - author={D.~Traytel and T.~Nipkow}, - title={{A} {V}erified {D}ecision {P}rocedure for {MSO} on - {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions}, - booktitle={Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)}, - pages={3-12}, - year=2013 -} - -@InProceedings{Coquand2012, - author = {T.~Coquand and V.~Siles}, - title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory}, - booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)}, - pages = {119--134}, - year = {2011}, - volume = {7086}, - series = {LNCS} -} - -@InProceedings{Almeidaetal10, - author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa}, - title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq}, - booktitle = {Proc.~of the 15th International Conference on Implementation - and Application of Automata (CIAA)}, - pages = {59-68}, - year = {2010}, - volume = {6482}, - series = {LNCS} -} - -@article{Owens2008, - author = {S.~Owens and K.~Slind}, - title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic}, - journal = {Higher-Order and Symbolic Computation}, - volume = {21}, - number = {4}, - year = {2008}, - pages = {377--409} -} - - -@article{Owens2, - author = {S.~Owens and K.~Slind}, - title = {Adapting functional programs to higher order logic}, - journal = {Higher-Order and Symbolic Computation}, - volume = {21}, - number = {4}, - pages = {377--409}, - year = {2008}, - url = {http://dx.doi.org/10.1007/s10990-008-9038-0}, - doi = {10.1007/s10990-008-9038-0}, - timestamp = {Wed, 16 Dec 2009 13:51:02 +0100}, - biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08}, - bibsource = {dblp computer science bibliography, http://dblp.org} -} - -@misc{PCRE, - title = "{PCRE - Perl Compatible Regular Expressions}", - url = {http://www.pcre.org}, -} +%% Saved with string encoding Unicode (UTF-8) -@InProceedings{OkuiSuzuki2010, - author = {S.~Okui and T.~Suzuki}, - title = {{D}isambiguation in {R}egular {E}xpression {M}atching via - {P}osition {A}utomata with {A}ugmented {T}ransitions}, - booktitle = {Proc.~of the 15th International Conference on Implementation - and Application of Automata (CIAA)}, - year = {2010}, - volume = {6482}, - series = {LNCS}, - pages = {231--240} -} +@url{SE16, + Author = {StackStatus}, + Date-Added = {2019-06-26 11:28:41 +0000}, + Date-Modified = {2019-06-26 11:42:11 +0000}, + Keywords = {ReDos Attack}, + Month = {07}, + Rating = {5}, + Read = {1}, + Title = {Stack Overflow Outage Postmortem}, + Url = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}, + Urldate = {2016.7.20}, + 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}} -@TechReport{OkuiSuzukiTech, - author = {S.~Okui and T.~Suzuki}, - title = {{D}isambiguation in {R}egular {E}xpression {M}atching via - {P}osition {A}utomata with {A}ugmented {T}ransitions}, - institution = {University of Aizu}, - year = {2013} -} +@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}, - 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}, - booktitle = {Proc.~of the 26th ACM Joint Meeting on European Software Engineering - Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)}, - year = {2018}, - pages = {246--256}, - numpages = {11} -} \ No newline at end of file + 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}}