Соревнования по формальной верификации VeHa-2024: накопленный в течение двух лет опыт и перспективы

В нашей статье описан опыт организации второго соревнования по формальной верификации программ среди молодых специалистов и студентов российских вузов. Соревнования проводились в связке с семинаром по семантике, спецификации и верификации программ (PSSV) в Иннополисе в октябре 2024 года. Формат соревнования был близок к формату так называемых хакатонов. Участникам было предложено решить на выбор 5 задач по верификации с использованием заранее определенных инструментов проверки моделей и дедуктивной верификации (Frama-C, Coq, C-lightVer, SPIN, TLC). Мы обсуждаем вопросы организации такого мероприятия, предложенные задачи, результаты решений и обратную связь от участников.

1. Старолетов С.М., Кондратьев Д.А., Гаранина Н.О., Шошмина И.В. Соревнования по формальной верификации VeHa-2023: опыт проведения // Труды Института системного программирования РАН. 2024, т. 36, № 2, с. 141-168.

2. 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.

3. 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.

4. TOOLympics Challenge 2023 / Ed. by D. Beyer, A. Hartmanns, F. Kordon. – Cham: Springer, 2025. – 172 p.

5. 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.

6. 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.

7. Denis X., Siegel S.F. VerifyThis 2023: An International Program Verification Competition. In TOOLympics Challenge 2023. TOOLympics 2024. Ser. LNCS. Springer, 2025, vol. 14550, pp. 147-159.

8. Jasper M., Mues M., Murtovi A., Schlüter 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.

9. 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.

10. 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.

11. 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.

12. Ernst G., Herber P., Huisman M., Ulbrich M. SpecifyThis Bridging Gaps Between Program Specification Paradigms: Track Introduction. In Proc. Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification. Ser. LNCS. Springer, 2025, vol. 15221, pp. 3-7.

13. 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.

14. 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.

15. 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.

16. 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.

17. 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.

18. 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.

19. VerifyThis Archive, 2024. Available at: https://www.pm.inf.ethz.ch/research/verifythis/Archive.html, accessed Nov 06, 2024.

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

21. VeHa2023 on GitHub. Available at: https://github.com/VeHaContest/VeHa2023, accessed Jul 06, 2024.

22. VeHa contest, 2024. Available at: https://sites.google.com/view/veha2024, accessed Nov 06, 2024.

23. VeHa2024 on GitHub. Available at: https://github.com/VeHaContest/VeHa2024, accessed Jul 06, 2024

24. NSU profile "Formal methods of program and system analysis". Available at https://education.nsu.ru/formal-analysis-methods/, accessed Dec 20, 2024.

25. Khazeev M., Aslam H., de Carvalho D., Mazzara M., Bruel JM., Brown J.A. Reflections on Teaching Formal Methods for Software Development in Higher Education. In: Proc. Frontiers in Software Engineering Education, ser. LNCS. Springer, 2020, vol 12271, pp. 28–41.

26. 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.

27. 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.

28. 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.

29. 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.

30. Khazeev M., Mazzara M., Aslam H., de Carvalho D. Towards a Broader Acceptance of Formal Verification Tools. In: Proc. Impact of the 4th Industrial Revolution on Engineering Education, ser. Advances in Intelligent Systems and Computing. Springer, 2020, vol. 1135, pp. 188–200.

31. 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.

32. 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.

33. 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.

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

35. 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.

36. 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.

37. 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.

38. Ahrendt W., Ernst G., Herber P., Huisman M., Monti R.E., Ulbrich M., Weigl A. The VerifyThis Collaborative Long-Term Challenge Series. In TOOLympics Challenge 2023. TOOLympics 2024. Ser. LNCS. Springer, 2025, vol. 14550, pp. 160-170.

39. 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.

40. 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.

41. 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.

42. Paul M., Haslbeck L., Wimmer S. Competitive Proving for Fun. In Selected Student Contributions and Workshop Papers of LuxLogAI 2018, vol. 10, pp. 9-14.

43. Paulin-Mohring C. Introduction to the Coq Proof-Assistant for Practical Software Verification. In Proc. Tools for Practical Software Verification. Ser. LNCS. Springer, 2012, vol. 7682, pp. 45-95.

44. 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.

45. 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.

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

47. 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.

48. 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.

49. The International Collegiate Programming Contest, ICPC. Available at https://icpc.global/, accessed Dec 21, 2024.

50. Chas K. The World's Smartest Programmers Compete: ACM ICPC. Communications of the ACM. Jul 2 2013. Available at https://cacm.acm.org/blogs/blog-cacm/165692-the-worlds-smartest-programmers-compete-acm-icpc/, accessed Dec 21, 2024.

51. Slamecka V.(editor) Proceedings of the 5th annual ACM computer science conference, CSC 1977, Atlanta, Georgia, USA, January 31 – February 2, 1977. ACM 1977, https://doi.org/10.1145/800008.808038.

52. Workshop "Program Semantics, Specification and Verification: Theory and Applications". Available at https://persons.iis.nsk.su/ru/PSSV-2024, accessed Dec 20, 2024.

53. Baudin P., Filliâtre J. C., Marché C., Monate B., Moy Y., & Prevosto V. (2008). Acsl: Ansi c specification language. CEA-LIST, Saclay, France, Tech. Rep. v1, 2.

54. Smalley S., Vance C., & Salamon W. (2001). Implementing SELinux as a Linux security module. NAI Labs Report, 1(43), 139.

55. Garanina N., Staroletov S., Gorlatch S. (2022, September). Model Checking Meets Auto-Tuning of High-Performance Programs. In International Symposium on Logic-Based Program Synthesis and Transformation (pp. 63-82). Cham: Springer International Publishing.

56. Garanina N., Staroletov S., Gorlatch S. Auto-Tuning High-Performance Programs Using Model Checking in Promela //arXiv preprint arXiv:2305.09130. – 2023.

57. GPGU Sim, manual. Revision 1.2 (GPGPU-Sim 3.1.1). Ed.: Tor M. Aamodt, Wilson W.L. Fung, Tayler H.Hetherington, http://gpgpu-sim.org/manual/index.php/Main_Page# Fetch_and_Decode_Software_Model, accessed Nov 06, 2024.

58. Lindholm E., Nickolls J., Oberman S., & Montrym J. (2008). NVIDIA Tesla: A unified graphics and computing architecture. IEEE micro, 28(2), 39-55.

59. Whitepaper “NVIDIA Tesla P100”. https://www.techpowerup.com/gpu-specs/docs/nvidia-gp100-architecture.pdf, accessed Nov 06, 2024.

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

61. 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.

62. Krom M.R. The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 13, no. 1-2, pp. 15-20, 1967.

63. Aspvall B., Plass M.F., Tarjan R.E. A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters, vol. 8, no. 3, pp. 121-123, 1979.

64. Myreen M.O., Davis J. The Reflective Milawa Theorem Prover Is Sound. In Proc. Interactive Theorem Proving. Ser. LNCS. Springer, 2014, vol. 8558, pp. 421-436.

65. Blanchette J.C., Fleury M., Lammich P, Weidenbach C. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. Journal of Automated Reasoning, vol. 61, no. 1, pp. 333–365, 2018.

66. Fleury M., Blanchette J.C., Lammich P. A verified SAT solver with watched literals using imperative HOL. In Proc. of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018, pp. 158–171.

67. Ciobâcă Ş., Andrici C.-C. A Verified Implementation of the DPLL Algorithm in Dafny. Mathematics, vol. 10, no. 13, article id: 2264, 2022.

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

69. Moniz H. (2020). The Istanbul BFT consensus algorithm. arXiv preprint arXiv:2002.03613.

70. Castro M., Liskov B. Practical Byzantine Fault Tolerance. Proceedings of the Third Symposium on Operating Systems Design and Implementation, New Orleans, USA, February 1999.

71. Pease M., Shostak R., Lamport L. Reaching Agreement in the Presence of Faults. Association for Computing Machinery, vol. 27, no. 2, 1980.

72. https://github.com/VeHaContest/VeHa2024/tree/main/solution_1_re_tofl, accessed Nov 06, 2024.

73. https://github.com/VeHaContest/VeHa2024/tree/main/solution_1_DevTools_Itmo, accessed Nov 06, 2024.

74. https://github.com/VeHaContest/VeHa2024/tree/main/solution_3_RARe, accessed Nov 06, 2024.

75. https://github.com/VeHaContest/VeHa2024/tree/main/solution_3_power_o%60_nine, accessed Nov 06, 2024.

76. Staroletov S. Teaching the discipline “Software Testing and Verification” to future programmers. System Informatics. vol. 21, pp. 1-28, 2022.