Open Access
Table 1
Analysis and comparison of related works
| Method | Algorithm | Derivation of algorithm | Verification of algorithm |
|---|---|---|---|
| Quantum and MapReduce[9] | Approximate edit distance algorithm | None | None |
| Random permutation model[10] | Window decomposition and novel sparsification edit distance algorithm | None | None |
| QRAM model[11] | Quantum linear edit distance algorithm | None | None |
| DaC, BFS-Hash[12] | Output-sensitive parallel edit distance algorithm | None | None |
| Mathematical derivation[2] | Dynamic programming algorithm |
Derivation of the recurrence relation | None |
| Formal divide and conquer[3] | Top-down and Bottom-top dynamic programming algorithm | Formal derivation of top-down and bottom-up dynamic programming | None |
| Functional model[6] | Dynamic programming algorithm of file comparison algorithm | Formal derivation of diagonal update and backward prime algorithm | Termination proof via a decreasing function and correctness verification through bisimulation and semantic consistency in Isabelle/HOL |
| Automatic memoization framework[4-5] | Six dynamic programming algorithms (such as edit distance and LCS algorithm) | Derivation of the monadification rules, memoization operation, and iterator design | Partly automatic verification in Isabelle/HOL, scalability issues remain unresolved |
| Formal model and verification condition generator (Ours) | Dynamic programming algorithm of edit distance | Formal derivation of recursive relations and loop invariants | Mechanical verification of five WP_verification conditions for edit distance in Isabelle/HOL |
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.