1 %% This BibTeX bibliography file was created using BibDesk. |
1 %% This BibTeX bibliography file was created using BibDesk. |
2 %% https://bibdesk.sourceforge.io/ |
2 %% https://bibdesk.sourceforge.io/ |
3 |
3 |
4 %% Created for CS TAN at 2022-11-20 17:26:32 +0000 |
4 %% Created for CS TAN at 2022-11-20 17:26:32 +0000 |
5 |
5 @inproceedings{LEX, |
6 |
6 title={Lex—a lexical analyzer generator}, |
|
7 author={Michael E. Lesk and Eric E. Schmidt}, |
|
8 year={1990}, |
|
9 url={https://api.semanticscholar.org/CorpusID:7900881} |
|
10 } |
|
11 @article{RegularExpressions, |
|
12 title={REPRESENTATION OF EVENTS IN NERVE NETS AND FINITE AUTOMATA$^1$}, |
|
13 author={Kleene, SC}, |
|
14 journal={Automata Studies: Annals of Mathematics Studies. Number 34}, |
|
15 number={34}, |
|
16 pages={3}, |
|
17 year={1956}, |
|
18 publisher={Princeton University Press} |
|
19 } |
7 %% Saved with string encoding Unicode (UTF-8) |
20 %% Saved with string encoding Unicode (UTF-8) |
8 @inproceedings{Doczkal2013, |
21 @inproceedings{Doczkal2013, |
9 author = {C.~Doczkaland J.O.~Kaiser and G.~Smolka}, |
22 author = {C.~Doczkaland J.O.~Kaiser and G.~Smolka}, |
10 title = {A Constructive Theory of Regular Languages in Coq}, |
23 title = {A Constructive Theory of Regular Languages in Coq}, |
11 year = {2013}, |
24 year = {2013}, |
682 howpublished = {\url{https://www.snort.org/faq/what-are-community-rules}}, |
695 howpublished = {\url{https://www.snort.org/faq/what-are-community-rules}}, |
683 note = {[Online; last accessed 19-November-2022]}, |
696 note = {[Online; last accessed 19-November-2022]}, |
684 title = {{Snort Community Rules}}, |
697 title = {{Snort Community Rules}}, |
685 year = {2022}} |
698 year = {2022}} |
686 |
699 |
|
700 @misc{Atom, |
|
701 howpublished = {\url{https://github.com/atom/atom}}, |
|
702 note = {[Online; last accessed 22-Aug-2023]}, |
|
703 title = {{Atom Editor}}, |
|
704 year = {2023}} |
|
705 |
|
706 @misc{fixedAtom, |
|
707 howpublished = {\url{http://davidvgalbraith.com/how-i-fixed-atom/}}, |
|
708 note = {[Online; last accessed 22-Aug-2023}}, |
|
709 title = {{How I fixed Atom}}, |
|
710 year = {2016}} |
|
711 |
|
712 |
|
713 @misc{Cloudflare, |
|
714 howpublished = {\url{https://www.cloudflare.com/en-gb/}}, |
|
715 note = {[Online; last accessed 22-Aug-2023}}, |
|
716 title = {{Cloudflare}}, |
|
717 year = {2023}} |
|
718 |
|
719 @misc{CloudflareOutage, |
|
720 howpublished = {\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}}, |
|
721 note = {[Online; last accessed 22-Aug-2023}}, |
|
722 title = {{Cloudflare}}, |
|
723 year = {2023}} |
|
724 |
|
725 @misc{TwainRegex, |
|
726 howpublished = {\url{https://zherczeg.github.io/sljit/regex_perf.html}}, |
|
727 %note = {[Online; last accessed 19-November-2022]}, |
|
728 author = {Zoltan Herczeg}, |
|
729 title = {{Performance comparison of regular expression engines}}, |
|
730 year = {2015}} |
|
731 |
687 @misc{KuklewiczHaskell, |
732 @misc{KuklewiczHaskell, |
688 author = {C.~Kuklewicz}, |
733 author = {C.~Kuklewicz}, |
689 keywords = {Buggy C POSIX Lexing Libraries}, |
734 keywords = {Buggy C POSIX Lexing Libraries}, |
690 title = {Regex Posix}, |
735 title = {Regex Posix}, |
691 url = {https://wiki.haskell.org/Regex_Posix}, |
736 url = {https://wiki.haskell.org/Regex_Posix}, |
855 series = {LNCS}, |
900 series = {LNCS}, |
856 title = {{V}erified {L}exical {A}nalysis}, |
901 title = {{V}erified {L}exical {A}nalysis}, |
857 volume = 1479, |
902 volume = 1479, |
858 year = 1998} |
903 year = 1998} |
859 |
904 |
|
905 @book{Isabelle, |
|
906 title={Isabelle/HOL: a proof assistant for higher-order logic}, |
|
907 author={Nipkow, Tobias and Paulson, Lawrence C and Wenzel, Markus}, |
|
908 volume={2283}, |
|
909 year={2002}, |
|
910 publisher={Springer Science \& Business Media} |
|
911 } |
|
912 |
|
913 |
860 @article{Brzozowski1964, |
914 @article{Brzozowski1964, |
861 author = {J.~A.~Brzozowski}, |
915 author = {J.~A.~Brzozowski}, |
862 journal = {Journal of the {ACM}}, |
916 journal = {Journal of the {ACM}}, |
863 number = {4}, |
917 number = {4}, |
864 pages = {481--494}, |
918 pages = {481--494}, |
1051 publisher="Springer International Publishing", |
1105 publisher="Springer International Publishing", |
1052 address="Cham", |
1106 address="Cham", |
1053 pages="533--560", |
1107 pages="533--560", |
1054 abstract="We present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. We build on top of Separation Logic with Time Credits, embedded in an interactive proof assistant. We formalize the O notation, which is key to enabling modular specifications and proofs. We cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. We propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples.", |
1108 abstract="We present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. We build on top of Separation Logic with Time Credits, embedded in an interactive proof assistant. We formalize the O notation, which is key to enabling modular specifications and proofs. We cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. We propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples.", |
1055 isbn="978-3-319-89884-1" |
1109 isbn="978-3-319-89884-1" |
|
1110 } |
|
1111 |
|
1112 |
|
1113 @article{ValiantParsing, |
|
1114 title={General Context-Free Recognition in Less than Cubic Time}, |
|
1115 author={Leslie G. Valiant}, |
|
1116 journal={J. Comput. Syst. Sci.}, |
|
1117 year={1975}, |
|
1118 volume={10}, |
|
1119 pages={308-315} |
|
1120 } |
|
1121 |
|
1122 |
|
1123 @inproceedings{bigOIsabelle, |
|
1124 title={Formalizing O notation in Isabelle/HOL}, |
|
1125 author={Avigad, Jeremy and Donnelly, Kevin}, |
|
1126 booktitle={International Joint Conference on Automated Reasoning}, |
|
1127 pages={357--371}, |
|
1128 year={2004}, |
|
1129 organization={Springer} |
|
1130 } |
|
1131 |
|
1132 |
|
1133 @inbook{subtypingFormalComplexity, |
|
1134 author = {Bessai, Jan and Rehof, Jakob and Düdder, Boris}, |
|
1135 year = {2019}, |
|
1136 month = {06}, |
|
1137 pages = {356-371}, |
|
1138 title = {Fast Verified BCD Subtyping}, |
|
1139 isbn = {978-3-030-22347-2}, |
|
1140 doi = {10.1007/978-3-030-22348-9_21} |
1056 } |
1141 } |
1057 %@article{10.1145/640128.604148, |
1142 %@article{10.1145/640128.604148, |
1058 %author = {Hofmann, Martin and Jost, Steffen}, |
1143 %author = {Hofmann, Martin and Jost, Steffen}, |
1059 %title = {Static Prediction of Heap Space Usage for First-Order Functional Programs}, |
1144 %title = {Static Prediction of Heap Space Usage for First-Order Functional Programs}, |
1060 %year = {2003}, |
1145 %year = {2003}, |
1091 %location = {New Orleans, Louisiana, USA}, |
1176 %location = {New Orleans, Louisiana, USA}, |
1092 %series = {POPL '03} |
1177 %series = {POPL '03} |
1093 %} |
1178 %} |
1094 |
1179 |
1095 |
1180 |
|
1181 %10.1145/3591262, |
|
1182 |
|
1183 @article{Margus2023PLDI, |
|
1184 author = {Moseley, Dan and Nishio, Mario and Perez Rodriguez, Jose and Saarikivi, Olli and Toub, Stephen and Veanes, Margus and Wan, Tiki and Xu, Eric}, |
|
1185 title = {Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics}, |
|
1186 year = {2023}, |
|
1187 issue_date = {June 2023}, |
|
1188 publisher = {Association for Computing Machinery}, |
|
1189 address = {New York, NY, USA}, |
|
1190 volume = {7}, |
|
1191 number = {PLDI}, |
|
1192 url = {https://doi.org/10.1145/3591262}, |
|
1193 doi = {10.1145/3591262}, |
|
1194 abstract = {We develop a new derivative based theory and algorithm for nonbacktracking regex matching that supports anchors and counting, preserves backtracking semantics, and can be extended with lookarounds. The algorithm has been implemented as a new regex backend in .NET and was extensively tested as part of the formal release process of .NET7. We present a formal proof of the correctness of the algorithm, which we believe to be the first of its kind concerning industrial implementations of regex matchers. The paper describes the complete foundation, the matching algorithm, and key aspects of the implementation involving a regex rewrite system, as well as a comprehensive evaluation over industrial case studies and other regex engines.}, |
|
1195 journal = {Proc. ACM Program. Lang.}, |
|
1196 month = {jun}, |
|
1197 articleno = {148}, |
|
1198 numpages = {24}, |
|
1199 keywords = {automata, derivative, symbolic, regex, PCRE, matching} |
|
1200 } |