EDP Sciences logo
Submit your paper
Search
Menu
All issues Volume 26 / No 6 (December 2021) Wuhan Univ. J. Nat. Sci., 26 6 (2021) 481-488 References
Open Access
Issue
Wuhan Univ. J. Nat. Sci.
Volume 26, Number 6, December 2021
Page(s) 481 - 488
DOI https://doi.org/10.1051/wujns/2021266481
Published online 17 December 2021
  1. Leino K R. Accessible software verification with Dafny [J]. IEEE Software , 2017, 34 (6): 94-97. [Google Scholar]
  2. Leino K R. Dafny: An automatic program verifier for functional correctness [C]// International Conference on Logic Programming .Berlin: Springer-Verlag, 2010: 348-370. [Google Scholar]
  3. 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]
  4. Leino K R, Monahan R. Dafny meets the verification benchmarks challenge [C]// Verified Software Theories Tools Experiments . Berlin: Springer-Verlag, 2010: 112-126. [CrossRef] [Google Scholar]
  5. Burstall R M, Darlington J. A transformation system for developing recursive programs [J]. Journal of the ACM , 1977, 24 (1): 44-67. [Google Scholar]
  6. Visser E. A survey of strategies in rule-based program transformation systems [J]. Journal of Symbolic Computation , 2005, 40 (1): 831-873. [CrossRef] [MathSciNet] [Google Scholar]
  7. Balog M, Gaunt A L, Brockschmidt M, et al . DeepCoder: Learning to write programs [C]// Proceedings of International Conference on Learning Representations . Washington D C : IEEE, 2017: 1-21. [Google Scholar]
  8. Bornholt J, Torlak E. Synthesizing memory models from framework sketches and litmus tests [J]. ACM SIGPLAN Notices , 2017, 52 (6): 467-481. [CrossRef] [Google Scholar]
  9. Brockschmidt M, Allamanis M, Gaunt A. Generative code modeling with graphs [C]// Proceedings of International Conference on Learning Representations . Louisiana: ICLR, 2019: 1-24. [Google Scholar]
  10. Exlcovisser. Program-transformation.org [EB/OL]. [2007- 02-14]. http://www.programtransformation.org . [Google Scholar]
  11. Pettorossi A, Proietti M. Automatic derivation of logic programs by transformation [J]. Course Notes for European Summer School on Logic, Language, and Information , 2000, 45 (1): 1-87. [Google Scholar]
  12. Secher J P. Unfold/Fold transformation, graduate course of university of copenhagen [EB/OL]. [2001-02-12]. http://www.diku.dk/topps/activities/pgmtrans/unfold-fold.ps . [Google Scholar]
  13. Pettorossi A, Proietti M. Program derivation = rules + strategies [C]// Computational Logic: Logic Programming and Beyond (Essays in Honour of Robert A. Kowalski-Part I) . Berlin: Springer-Verlag, 2002: 273-309. [Google Scholar]
  14. Morgan C. Programming from Specifications [M]. Oxford: Oxford University Press, 1991. [Google Scholar]
  15. Pavlovic D, Smith D R. Software development by refinement [C]// Formal Methods at the Crossroads: From Panaea to Foundational Support, LNCS . Berlin: Springer-Verlag, 2003: 267-286. [Google Scholar]
  16. Wang X, Dillig I, Singh R. Program synthesis using abstraction refinement [J]. Proceedings of the ACM on Programming Languages , 2017, 45 (2): 1-31. [Google Scholar]
  17. Leavens G T, Abrial J R, Batory D. Roadmap for enhanced languages and methods to aid verification [C]// 5th Int’l Conf on Generative Programming and Component Engineering . Philadelphia: ACM Press, 2006: 221-236. [CrossRef] [Google Scholar]
  18. Xue J Y, You Z, Hu Q. PAR: A practicable formal method and its supporting platform [C]// International Conference on Formal Engineering Methods . Berlin: Springer-Verlag. 2018: 70-86. [Google Scholar]
  19. You Z, Xue J Y. Formal verification of algorithmic programs based on the Isabelle theorem prover [J]. Computer Engineering and Science , 2009, 31 (10): 85-89(Ch). [NASA ADS] [Google Scholar]
  20. Barnett M, Leino K R M, Schulte W. The spec# programming system: An overview [C]// International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices . Berlin: Springer-Verlag, 2004: 1-20. [Google Scholar]
  21. Fisler K, Krishnamurthi S. Modular verification of collaboration-based software designs [C]// European Software Engineering Conference; ESEC; ACM SIGSOFT Symposium on the Foundations of Software Engineering; FSE-9 . Washington D C: IEEE, 2001: 10-14. [Google Scholar]
  22. Barnett M, Chang B E, Deline R, et al . Boogie: A modular reusable verifier for object-oriented programs [C]// 4th International Symposium Lecture Notes in Computer Science , Berlin: Springer-Verlag, 2006: 364-387. [CrossRef] [Google Scholar]
  23. Moura L D, Bjorner N. Z3: An efficient SMT solver [C]// Tools and Algorithms for Construction and Analysis of Systems . Berlin: Springer-Verlag, 2008: 337-340. [Google Scholar]
  24. Leino K R. Automating induction with an SMT solver [C]// Proc 13th Int’l Conf Verification, Model Checking, and Abstract Interpretation . Berlin: Springer-Verlag, 2012: 315-331. [Google Scholar]
  25. Hu Q M, Xue J Y, You Z, et al . Research on the formal verification technology of several software components in the PAR platform [J]. Computer Engineering and Science , 2018, 40 (2): 268-274(Ch). [Google Scholar]
  26. Wang C J, He J F, Luo H M, et al . Model-driven formal generation and automatic validation of Dafny programs [J]. Journal of Jiangxi Normal University , 2020, 44 (4): 378-384(Ch). [Google Scholar]
  27. Wang C J, Yu X J, Shen D M, et al .A two-layer verification method for concurrent distributed shared memory algorithm based on concurrent Apla [J]. Journal of Jiangxi Normal University , 2020, 44 (3): 301-306(Ch). [Google Scholar]
  28. Zuo Z K, Fang Y, Huang Q, et al .Nonrecursive binary tree sorting algorithm and its formal proof [J]. Journal of Jiangxi Normal University , 2020, 44 (6): 625-6329(Ch). [Google Scholar]
  29. Zuo Z K, Lu Z H, Huang Q, et al . A comparative study of generic features between Apla and programming languages [J]. Journal of Jiangxi Normal University , 2019, 43 (5): 454-461(Ch). [Google Scholar]
  30. Zhou W X, Zuo Z K, WANG C J, et al . The contrastive study of generic programming in object-oriented languages [J]. Journal of Jiangxi Normal University , 2018, 42 (3): 304-310(Ch). [Google Scholar]
  31. Zhang Q, Wang C J, Luo H M, et al . The generation method and automatical transformation system of WSDL→Radl-WS [J]. Journal of Jiangxi Normal University , 2018, 42 (3): 298-30(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.