Open Access
| Issue |
Wuhan Univ. J. Nat. Sci.
Volume 30, Number 6, December 2025
|
|
|---|---|---|
| Page(s) | 576 - 588 | |
| DOI | https://doi.org/10.1051/wujns/2025306576 | |
| Published online | 09 January 2026 | |
- Wang J, Zhan N J, Feng X Y, et al. Overview of formal methods[J]. Journal of Software, 2019, 30(1): 33-61(Ch). [Google Scholar]
- Dasgupta S, Papadimitriou C H, Vazirani U V. Algorithms[M]. New York: McGraw-Hill Education, 2006. [Google Scholar]
- Mofarah-Fathi L, Norvell T S. Formal derivation of dynamic programming algorithms[EB/OL].[2007-11-26]. https://www.engr.mun.ca/~theo/Publications/submittedNECEC2007.pdf. [Google Scholar]
- Wimmer S, Hu S W, Nipkow T. Verified memoization and dynamic programming[M]//Interactive Theorem Proving. Cham: Springer-Verlag, 2018. [Google Scholar]
- Wimmer S, Hu S W, Nipkow T. Monadification, memoization and dynamic programming[EB/OL]. [2018-10-25]. https://www.isa-afp.org/browser_info/current/AFP/Monad_Memo_DP/document.pdf. [Google Scholar]
- Song L H, Wang H T, Ji X J, et al. Verification of file comparison algorithm fcomp in Isabelle/HOL[J]. Journal of Software, 2017, 28(2): 203-215(Ch). [Google Scholar]
- Nipkow T, Klein G. Concrete Semantics: With Isabelle/HOL[M]. Cham: Springer-Verlag, 2023. [Google Scholar]
- Si X J, Dai H J, Raghothaman M, et al. Learning loop invariants for program verification[C]// Proceedings of the 32nd International Conference on Neural Information Processing Systems. Montréal: Curran Associates Inc, 2018: 7762-7773. [Google Scholar]
- Boroujeni M, Ehsani S, Ghodsi M, et al. Approximating edit distance in truly subquadratic time: Quantum and MapReduce[J]. Journal of the ACM , 2021, 68(3): 1-41. [Google Scholar]
- Boroujeni M, Seddighin M, Seddighin S. Improved algorithms for edit distance and LCS: Beyond worst case[C]//Proceedings of the 14th Annual ACM-SIAM Symposium on Discrete Algorithms. Philadelphia: Society for Industrial and Applied Mathematics, 2020: 1601-1620. [Google Scholar]
- Equi M, Griend A M, Mäkinen V. Quantum linear algorithm for edit distance using the word QRAM model[EB/OL]. [2021-03-30]. https://arXivpreprintarXiv:2112.13005. [Google Scholar]
- Ding X, Dong X, Gu Y, et al. Efficient parallel output-sensitive edit distance[EB/OL]. [2023-04-21]. https://www.semanticscholar.org/reader/6b2439fa153e2e6feace3d69f1167f8d41172328. [Google Scholar]
- Eddy S R. What is dynamic programming[J]. Nature Biotechnology, 2004, 22(7): 909-910. [CrossRef] [Google Scholar]
- Luus R. Iterative Dynamic Programming[M]. New York: Chapman and Hall/CRC, 2000. [Google Scholar]
- Hoare C A R. An axiomatic basis for computer programming[J]. Communications of the ACM, 1969, 12(10): 576-580. [Google Scholar]
- Zuo Z K, Hu Y, Huang Q, et al. Automatic algorithm programming model based on the improved Morgan's refinement calculus[J]. Wuhan University Journal of Natural Sciences, 2022, 27(5): 405-414. [CrossRef] [EDP Sciences] [Google Scholar]
- Paulson L C, Nipkow T, Wenzel M. From LCF to Isabelle/HOL[J]. Formal Aspects of Computing, 2019, 31(6): 675-698. [Google Scholar]
- Jiang N, Li Q G, Wang L, et al. Overview on mechanized theorem proving[J]. Journal of Software, 2020, 31(1): 82-112(Ch). [Google Scholar]
- Zuo Z K, Sun H, Wang C J, et al. Program derivation and mechanized verification of imperative dynamic programming algorithms[J]. International Journal of Software and Informatics, 2024, 14(4): 419-448. [Google Scholar]
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.