equal
deleted
inserted
replaced
4 %% Created for CS TAN at 2022-03-16 16:38:47 +0000 |
4 %% Created for CS TAN at 2022-03-16 16:38:47 +0000 |
5 |
5 |
6 |
6 |
7 %% Saved with string encoding Unicode (UTF-8) |
7 %% Saved with string encoding Unicode (UTF-8) |
8 |
8 |
9 |
9 @article{Rathnayake2014StaticAF, |
|
10 title={Static Analysis for Regular Expression Exponential Runtime via Substructural Logics}, |
|
11 author={Asiri Rathnayake and Hayo Thielecke}, |
|
12 journal={ArXiv, |
|
13 year={2014}, |
|
14 volume={abs/1405.7058} |
|
15 } |
10 |
16 |
11 @inproceedings{RibeiroAgda2017, |
17 @inproceedings{RibeiroAgda2017, |
12 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.}, |
18 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.}, |
13 address = {New York, NY, USA}, |
19 address = {New York, NY, USA}, |
14 articleno = {4}, |
20 articleno = {4}, |