Open Access
Issue |
Wuhan Univ. J. Nat. Sci.
Volume 28, Number 3, June 2023
|
|
---|---|---|
Page(s) | 246 - 256 | |
DOI | https://doi.org/10.1051/wujns/2023283246 | |
Published online | 13 July 2023 |
- Gu T L. The Formal Method of Software Development[M]. Beijing: Higher Education Press, 2005(Ch). [Google Scholar]
- Wang J, Zhan N J, Feng X Y , et al. An overview of formal methods [J]. Journal of Software, 2019, 30(1): 33-61(Ch). [Google Scholar]
- Michael J B, Dinolt G W, Drusinsky D. Open questions in formal methods [J]. IEEE Annals of the History of Computing, 2020, 53(5): 81-84. [CrossRef] [Google Scholar]
- Xue J, Zheng Y, Hu Q, et al. PAR: A practicable formal method and its supporting platform[C]// International Conference on Formal Engineering Methods. Cham: Springer-Verlag, 2018: 70-86. [Google Scholar]
- Dijkstra E W. A Discipline of Programming [M]. Englewood Cliffs: Prentice Hall, 1976. [Google Scholar]
- Dijkstra E W , Feijen W. A Method of Programming[M]. Boston: Addison-Wesley Longman Publishing Co. Inc., 1988. [Google Scholar]
- Morgan C. Programming from Specifications[M]. Upper Saddle River : Prentice-Hall, Inc., 1990. [Google Scholar]
- Kourie D G, Watson B W. The Correctness-by-Construction Approach to Programming[M]. Berlin: Springer Science & Business Media, 2012. [CrossRef] [Google Scholar]
- Runge T , Schaefer I , Cleophas L , et al. Tool support for correctness-by-construction[C]//International Conference on Fundamental Approaches to Software Engineering. Berlin: Springer-Verlag, 2019: 25-42. [Google Scholar]
- Si X, Dai H J, Raghothaman M, et al. Learning loop invariant for program verification[C]//Proceedings of the 32nd International Conference on Neural Information Processing Systems. Montreal: Neural Information Processing Systems Foundation, 2018. [Google Scholar]
- Gries D. A note on a standard strategy for developing loop invariant and loops[J]. Science of Computer Programming, 1982, 2(3): 207-214. [CrossRef] [MathSciNet] [Google Scholar]
- Nipkow T, Klein G. Concrete Semantics with Isabelle/HOL[M]. Berlin: Springer International Publishing, 2014. [CrossRef] [Google Scholar]
- Nipkow T, Markus W, Lawrence C. Isabelle/HOL: A Proof Assistant for Higher-Order Logic[M]. Berlin, Heidelberg: Springer-Verlag, 2002. [Google Scholar]
- Benzmüller C , Claus M , Sultana N. Systematic verification of the modal logic cube in Isabelle / HOL[J] . Electronic Proceedings in Theoretical Computer Science, 2015, 186: 27-41. [CrossRef] [MathSciNet] [Google Scholar]
- Lai Y. Development of APLA to C++ Automatic Program Conversion System [D]. Nanchang : Jiangxi Normal University, 2002(Ch). [Google Scholar]
- Jiang N, Li Q A, Wang L M, et al. Review of mechanized theorem proof research [J]. Journal of Software, 2020, 31(1): 82-112(Ch). [Google Scholar]
- Tobias N K, Lawrence P S. Auxiliary Proof System for Higher Order Logic[M]. Beijing: Institute of Technology Press, 2013(Ch). [Google Scholar]
- Zuo Z K, Fang Y, Huang Q, et al. Derivation and formal proof of binary tree sorting non-recursive Algorithm[J]. Journal of Jiangxi Normal University(Natural Science Edition), 2020, 44(6): 625-632(Ch) . [Google Scholar]
- You Z, Xue J Y. Formal verification of algorithm program based on Isabelle theorem prover[J]. Computer Engineering and Science, 2009, 31(10): 85-89(Ch). [NASA ADS] [Google Scholar]
- Zhang Q F, Wang C J, Zuo Z K, et al. The formal verification method for smart contract properties based on UPPAAL[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2023, 47(1): 45-51(Ch). [Google Scholar]
- Wang C J, Chen X, Ding X L, et al. The Web service symbolic execution and verification based on model-driven[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2022, 46(1): 37-48(Ch). [Google Scholar]
- Zuo Z K, Fang Y, Huang Z P, et al. The derivation and formal proof of non-recursive algorithm for binary tree queue relation problems[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2022, 46(1): 49-58(Ch). [Google Scholar]
- Yu X J, Wang C J, Qu W J, et al. The prediction of epidemic trend of COVID-19[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2021, 45(6): 559-565(Ch). [Google Scholar]
- Wang C J, He J F, Luo H M, et al. The model-driven Dafny program generation and automatic verification[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2020, 44(4): 378-384(Ch). [Google Scholar]
- Wang C J, Yu X J, Shen D M, et al. The two-level verification method of shared memory concurrent distributed algorithm based on concurrent Apla language[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2020, 44(3): 301-306(Ch). [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.