Соревнования по формальной верификации VeHa-2023: опыт проведения

Для создания современного конкурентоспособного и доверенного программного обеспечения необходимо использовать знания формальных методов. В настоящее время огромное количество студентов обучается специальностям, связанным с программированием. Однако при обучении в вузе сложно получить навык практического применения теоретических знаний. Короткие соревнования с нестандартными близкими к промышленным задачами могут пробудить интерес студентов к области формальных методов. В нашей статье описан первый опыт организации соревнования по формальной верификации программ среди студентов российских вузов. Соревнования проводились в связке с семинаром по семантике, спецификации и верификации программ (PSSV) в Иннополисе в ноябре 2023 года. Формат соревнования был близок к формату так называемых хакатонов. Участникам было предложено решить задачи по верификации с использованием заранее определенных инструментов проверки моделей и дедуктивной верификации. Мы рассмотрим вопросы организации такого мероприятия, предложенные задачи, результаты решений и обратную связь от участников.

1. PSSV 2023. Available at: https://persons.iis.nsk.su/en/PSSVfrom2022towards2023, accessed Jul 06,2024.

2. Zavyalov A., Staroletov S. Flovver: A graphical functional language with a compiler focused on recursion optimization. Computing, Telecommunications and Control, vol. 16, no. 1, pp. 46–59, 2023.

3. Hackathon Barnaul 2023. Available at: https://innovaltai.ru/sobytiya/detail.php?ID=3161, accessed Jul 06, 2024.

4. Participants in the Neftecode hackaton have developed solutions that will help build more durable roads in Russia, 2022. Available at: https://news.itmo.ru/ru/startups_and_business/partnership/news/12855/, accessed Jul 06, 2024.

5. Tender Hack, 2023. Available at: https://tenderhack.ru/tenderhack-kazan.pdf?roistat_visit=1154183, accessed Jul 06, 2024.

6. Sadovykh A., Beketova M., Khazeev M. Hackathons as a part of software engineering education: Case in tools example. In Proc. Frontiers in Software Engineering Education: First International Workshop, FISEE 2019, Villebrumier, France, 2019, Invited Papers 1. November 11–13, Springer, 2020, pp. 232–245.

7. Hoare C. A. R. An axiomatic basis for computer programming. Communications of the ACM, vol. 12, no. 10, pp. 576–580, 1969.

8. Apt K. R., Olderog E.-R. Assessing the success and impact of Hoare’s logic. In Proc. Theories of Programming: The Life and Works of Tony Hoare, 2021, pp. 41–76.

9. Apt K. R., Olderog E.-R. Fifty years of Hoare’s logic. Formal Aspects of Computing, vol. 31, no. 6, pp. 751– 807, 2019.

10. Filliâtre J.-C. Deductive software verification. International Journal on Software Tools for Technology Transfer, vol. 13, no. 5, pp. 397–403, 2011.

11. Clarke J., Emerson E. Design and synthesis of synchronization skeletons using branching time temporal logic. In proc. Logic of Programs: Workshop, Yorktown Heights, ser. LNCS. Springer, 1981, vol. 131, pp. 52–71.

12. Quielle J., Sifakis J. Specification and verification of concurrent systems in CESAR. In Proc. of the 5th International Symposium on Programming, ser. LNCS. Springer, 1982, vol. 137, pp. 337–350.

13. Hähnle R., Huisman M. Deductive software verification: From pen-and-paper proofs to industrial tools. In Proc. Of Computing and Software Science, ser. LNCS. Springer, 2019, vol. 10000, pp. 345-373.

14. Furia C. A., Meyer B., Velder S. Loop invariants: Analysis, classification, and examples. ACM Computing Surveys, vol. 46, no. 3, pp. 1–51, 2014.

15. Ernst G. Loop verification with invariants and contracts. In Proc. Verification, Model Checking, and Abstract Interpretation, ser. LNCS. Springer, 2022, vol. 13182, pp. 69–92.

16. First E., Brun Y. Diversity-driven automated formal verification. In Proc. of the 44th International Conference on Software Engineering, 2022, pp. 749–761.

17. Maryasov I. V., Nepomniaschy V. A., Promsky A. V., Kondratyev D. A. Automatic C program verification based on mixed axiomatic semantics. Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 407–414, 2014.

18. Kondratyev D. A., Promsky A. V. Developing a self-applicable verification system. Theory and practice. Automatic Control and Computer Sciences, vol. 49, no. 7, pp. 445–452, 2015.

19. Kondratyev D. A., Nepomniaschy V. A. Automation of C program deductive verification without using loop invariants. Programming and Computer Software, vol. 48, no. 5, pp. 331–346, 2022.

20. Nepomniaschy V. A., Anureev I. S., Mikhailov I. N., Promskii A. V. Towards verification of C programs. C-Light language and its formal semantics. Programming and Computer Software, vol. 28, no. 6, pp. 314–323, 2002.

21. Nepomniaschy V. A., Anureev I. S., Promskii A. V. Towards verification of C programs: Axiomatic semantics of the C-kernel language. Programming and Computer Software, vol. 29, no. 6, pp. 338–350, 2003.

22. Cuoq P., Monate B., Pacalet A., Prevosto V. Functional dependencies of C functions via weakest pre-conditions. International Journal on Software Tools for Technology Transfer, vol. 13, no. 5, pp. 405–417, 2011.

23. Correnson L. Qed. Computing what remains to be proved. In Proc. NASA Formal Methods, ser. LNCS. Springer, 2014, vol. 8430, pp. 215–229.

24. Baudin P., Bobot F., Bühler D., Correnson L., Kirchner F., Kosmatov N., Maroneze A., Perrelle V., Prevosto V., Signoles J., Williams N. The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Communications of the ACM, vol. 64, no. 8, pp. 56–68, 2021.

25. Mandrykin M. U., Khoroshilov A. V. High-level memory model with low-level pointer cast support for Jessie intermediate language. Programming and Computer Software, vol. 41, no. 4, pp. 197–207, 2015.

26. Mandrykin M. U., Khoroshilov A. V. Region analysis for deductive verification of C programs. Programming and Computer Software, vol. 42, no. 5, pp. 257–278, 2016.

27. Mandrykin M. U., Khoroshilov A. V. Towards deductive verification of C programs with shared data. Programming and Computer Software, vol. 42, no. 5, pp. 324–332, 2016.

28. Efremov D., Mandrykin M., Khoroshilov A. Deductive verification of unmodified Linux kernel library functions. In Proc. Leveraging Applications of Formal Methods, Verification and Validation. Verification, ser. LNCS. Springer, 2018, vol. 11245, pp. 216–234.

29. Volkov G., Mandrykin M. Efremov D. Lemma functions for Frama-C: C programs as proofs. In Proc. 2018 Ivannikov Ispras Open Conference (ISPRAS), 2018, pp. 31–38.

30. Sammler M., Lepigre R., Krebbers R., Memarian K., Dreyer D., Garg D. RefinedC: automating the foundational verification of C code with refined ownership types. In Proc. of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021, pp. 158–174.

31. Lepigre R., Sammler M., Memarian K., Krebbers R., Dreyer D., and Sewell P. VIP: verifying real-world C idioms with integer-pointer casts. In Proc. vol. 6 POPL, 2022, pp. 1–32.

32. Kondratyev D. A., Maryasov I. V., Nepomniaschy V. A. The automation of C program verification by the symbolic method of loop invariant elimination. Automatic Control and Computer Sciences, vol. 53, no. 7, pp. 653–662, 2019.

33. Nepomniaschy V. A. Symbolic method of verification of definite iterations over altered data structures. Programming and Computer Software, vol. 31, no. 1, pp. 1–9, 2005.

34. Moore J. S. Milestones from the pure Lisp theorem prover to ACL2. Formal Aspects of Computing, vol. 31, no. 6, pp. 699–732, 2019.

35. Cimatti A., Clarke E., Giunchiglia E., Giunchiglia F., Pistore M., Roveri M., Sebastiani R., Tacchella A. NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), ser. LNCS, vol. 2404. Copenhagen, Denmark: Springer, 2002.

36. Kwiatkowska M., Norman G., Parker D. PRISM 4.0: Verification of probabilistic real-time systems. In Proc. Computer Aided Verification, ser. LNCS. Springer Berlin Heidelberg, 2011, pp. 585–591.

37. Visser W., Pǎsǎreanu C., Khurshid S. Test input generation with java PathFinder. In Proc. of the ACM/SIGSOFT International Symposium on Software Testing and Analysis. ACM Press, 2004, pp. 97– 107.

38. Hessel A., Larsen K., Mikucionis M., Nielsen B., Pettersson P., Skou A. Testing real-time systems using Uppaal. In Proc. Formal Methods and Testing, 2008, pp. 77–117.

39. Kuppe M. A., Lamport L., Ricketts D. The TLA+ toolbox. In Proc. Fifth Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7th October 2019, ser. EPTCS, R. Monahan, V. Prevosto, and J. Proenca, Eds., vol. 310, 2019, pp. 50–62.

40. Holzmann G. J. The Spin model checker, primer and reference manual. 2003.

41. Victor Duarte da Silva. Syntax highlighting for Promela and Spin Simulation on debugger. Available at: https://marketplace.visualstudio.com/items?itemName=dsvictor94.promela, accessed Jul 06, 2024.

42. Jacobs B., Kiniry J. Warnier M. Java program verification challenges. In Proc. Formal Methods for Components and Objects, ser. LNCS. Springer, 2003, vol. 2852, pp. 202–219.

43. Leavens G. T., Leino K. R. M., Müller P. Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing, vol. 19, no. 2, pp. 159– 189, 2007.

44. Leino K. R. M., Moskal M. VACID-0: verification of ample correctness of invariants of data-structures, edition 0. In Proc. of Tools and Experiments Workshop at VSTTE, 2010.

45. Weide B. W., Sitaraman M., Harton H. K., Adcock B., Bucci P., Bronish D., Heym W. D., Kirschenbaum J., Frazier D. Incremental benchmarks for software verification tools and techniques. In Proc. Verified Software: Theories, Tools, Experiments, ser. LNCS. Springer, 2008, vol. 5295, pp. 84–98.

46. Huisman M., Klebanov V., Monahan R. VerifyThis 2012. International Journal on Software Tools for Technology Transfer, vol. 17, no. 6, pp. 647–657, 2015.

47. Hoare C. A. R., Leavens G. T., Shankar N. The verified software initiative: A manifesto. ACM Computing Surveys, vol. 41, no. 4, pp. 1–8, 2009.

48. Müller P., Shankar N. The first fifteen years of the verified software project. In Proc. Theories of Programming: The Life and Works of Tony Hoare, 2021, pp. 93–124.

49. Klebanov V., Müller P., Shankar N., Leavens G. T., Wüstholz V., Alkassar E., Arthan R., Bronish D., Chapman R., Cohen E., Hillebrand M., Jacobs B., Leino K. R. M., Monahan R., Piessens F., Polikarpova N., Ridge T., Smans J., Tobies S., Tuerk T., Ulbrich M., Weiß B. The 1st verified software competition: Experience report. In Proc. FM 2011: Formal Methods, ser. LNCS. Springer, 2011, vol. 6664, pp. 154 – 168.

50. Filliâtre J.-C., Paskevich A., Stump A. The 2nd verified software competition: Experience report. In Proc. of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, ser. CEUR Workshop Proceedings. RWTH Aachen University, 2012, vol. 873, pp. 36–49.

51. Bormer T., Brockschmidt M., Distefano D., Ernst G., Filliâtre J.-C., Grigore R., Huisman M., Klebanov V., Marché C., Monahan R., Mostowski W., Polikarpova N., Scheben C., Schellhorn G., Tofan B., Tschannen J., Ulbrich M. The COST IC0701 verification competition 2011. In Proc. Formal Verification of Object-Oriented Software, ser. LNCS. Springer, 2012, vol. 7421, pp. 3–21.

52. Huisman M., Klebanov V., Monahan R. On the organisation of program verification competitions. In Proc. of the 1st International Workshop on Comparative Empirical Evaluation of Reasoning Systems, ser. CEUR Workshop Proceedings. RWTH Aachen University, 2012, vol. 873, pp. 50–59.

53. Beyer D., Huisman M., Klebanov V., Monahan R. Evaluating software verification systems: Benchmarks and competitions (Dagstuhl reports 14171). Dagstuhl Reports, vol. 4, no. 4, pp. 1–19, 2014.

54. Huisman M., Klebanov V., Monahan R., Tautschnig M. VerifyThis 2015. International Journal on Software Tools for Technology Transfer, vol. 19, no. 6, pp. 763–771, 2017.

55. Dross C., Furia C. A., Huisman M., Monahan R., Müller P. VerifyThis 2019: a program verification competition. International Journal on Software Tools for Technology Transfer, vol. 23, no. 6, pp. 883–893, 2021.

56. Ernst G., Huisman M., Mostowski W., Ulbrich M. VerifyThis – verification competition with a human factor. In Proc. Tools and Algorithms for the Construction and Analysis of Systems. Ser. LNCS. Springer, 2019, vol. 11429, pp. 176-195.

57. Huisman M., Monti R., Ulbrich M., Weigl A. The VerifyThis collaborative long term challenge. In Proc. Deductive Software Verification: Future Perspectives, ser. LNCS. Springer, 2020, vol. 12345, pp. 246 – 260.

58. Ernst G. Weigl A. Verify This: Memcached–a practical long-term challenge for the integration of formal methods. In Proc. iFM 2023, ser. LNCS. Springer, 2024, vol. 14300, pp. 82–89.

59. Bartocci E., Beyer D, Black P. E., Fedyukovich G., Garavel H., Hartmanns A., Huisman M., Kordon F., Nagele J., Sighireanu M., Steffen B., Suda M., Sutcliffe G., Weber T., Yamada A. TOOLympics 2019: An overview of competitions in formal methods. In Proc. Tools and Algorithms for the Construction and Analysis of Systems, ser. LNCS. Springer, 2019, vol. 11429, pp. 3–24.

60. Beyer D., Huisman M., Kordon F., Steffen B. TOOLympics II: competitions on formal methods. International Journal on Software Tools for Technology Transfer, vol. 23, no. 6, pp. 879–881, 2021.

61. Jasper M., Mues M., Murtovi A., Schluter M., Howar F., Steffen B., Schordan M., Hendriks D., Schiffelers R., Kuppens H., Vaandrager F. W. RERS 2019: Combining synthesis with real-world models. In Tools and Algorithms for the Construction and Analysis of Systems, ser. LNCS. Springer, 2019, vol. 11429, pp. 101–115.

62. Geske M., Jasper M., Steffen B., Howar F., Schordan M., van de Pol J. Rers 2016: Parallel and sequential benchmarks with focus on LTL verification. In Proc. Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, ser. LNCS. Springer, 2016, vol. 9953, pp. 787–803.

63. Jasper M., Fecke M., Steffen B., Schordan M., Meijer J., van de Pol J., Howar F., Siegel S. F. The Rers 2017 challenge and workshop (invited paper). In Proc. of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017, pp. 11–20.

64. Jasper M., Mues M., Schlüter M., Steffen B, Howar F. Rers 2018: CTL, LTL, and reachability. In Proc. Leveraging Applications of Formal Methods, Verification and Validation of Systems, ser. LNCS. Springer, 2018, vol. 11245, pp. 433-447.

65. Howar F., Jasper M., Mues M., Schmidt D., Steffen B. The Rers challenge: towards controllable and scalable benchmark synthesis. International Journal on Software Tools for Technology Transfer, vol. 23, no. 6, pp. 917– 930, 2021.

66. Giesl J., Rubio A., Sternagel C., Waldmann J., Yamada A. The termination and complexity competition. In Proc. Tools and Algorithms for the Construction and Analysis of Systems, ser. LNCS. Springer, 2019, vol. 11429, pp. 156–166.

67. Marché C., Zantema H. The termination competition. In Proc. Term Rewriting and Applications, ser. LNCS. Springer, 2007, vol. 4533, pp. 303–313.

68. Giesl J, Mesnard F., Rubio A., Thiemann R., Waldmann J. Termination competition (TermCOMP 2015). In Proc. Automated Deduction - CADE-25, ser. LNCS. Springer, 2015, vol. 9195, pp. 105–108.

69. Yamada A. Termination of term rewriting: Foundation, formalization, implementation, and competition. In Proc. 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), ser. Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl – Leibniz-Zentrum fur Informatik, 2023, vol. 260, pp. 4:1–4:5.

70. Ahrendt W., Herber P., Huisman M., Ulbrich M. SpecifyThis – bridging gaps between program specification paradigms. In Proc. Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, ser. LNCS. Springer, 2022, vol. 13701, pp. 3-6.

71. VeHa contest, 2023. Available at: https://sites.google.com/view/veha23/, accessed Jul 06, 2024.

72. The First Computer Bug, 1945. Available at: https://commons.wikimedia.org/wiki/File:First_Computer_Bug,_1945.jpg, accessed Jul 06, 2024.

73. GitHub, Inc, Creating a pull request, 2023. Available at: https://docs.github.com/en/pull- requests/collaborating-with-pull-requests/proposing-changes-to-your-work-with-pull-requests/creating-a-pull-request, accessed Jul 06, 2024.

74. VeHaContest2023 on GitHub. Available at: https://github.com/SergeyStaroletov/VeHaContest2023, accessed Jul 06, 2024.

75. Luna 25 mission, RBC. Available at: https://www.rbc.ru/technology_and_media/03/10/2023/651bbeab9a794768782f8d0d, accessed Jul 06, 2024.

76. Luna-25 mission, 2023. Available at: https://www.roscosmos.ru/39790/, accessed Jul 06, 2024.

77. Garanina N., Staroletov S., Gorlatch S. Model checking meets auto-tuning of high-performance programs,” in International Symposium on Logic-Based Program Synthesis and Transformation. Springer, 2022, pp. 63-82.

78. Khronos. OpenCL Specification by Khronos Working Group, 2021. Available: https://www.khronos.org/registry/OpenCL/specs/3.0-unified/html/OpenCL_API.html, accessed Jul 06, 2024.

79. Tor A. GPGPU-Sim. Available at: http://gpgpu-sim.org, accessed Jul 06, 2024.

80. Staroletov S. Towards Modeling and Verification of Eurobalise Telegram Encoding Algorithm. Transportation Research Procedia, vol. 61, pp. 447–454, 2022.

81. Basics of Software Testing and Verification (in Russian). Lanbook publishing, Saint Petersburg, p. 344, 2020. – EDN SGQVLL. Available at: https://e.lanbook.com/book/319445, accessed Jul 06, 2024.

82. An Efficient Logic Model Checker for the Verification of threaded Code, 2023. Available at: https://github.com/nimble-code/Spin, accessed Jul 06, 2024.

83. select - non-deterministic value selection, 2021. Available at: http://spinroot.com/spin/Man/select.html, accessed Jul 06, 2024.