VeHa-2024 Formal Verification Contest: Two Years of Experience and Prospects
Dmitry Alexandrovich KONDRATYEV,
Sergey Mikhailovich STAROLETOV,
Irina Vladimirovna SHOSHMINA,
Anastasiya Vladimirovna KRASNENKOVA,
Kirill Viktorovich ZIBOROV,
Nikolay Vyacheslavovich SHILOV,
Natalia Olegovna GARANINA,
Timofey Yuryevich CHERGANOV https://doi.org/10.15514/ISPRAS-2025-37(1)-10
Abstract
We present our experience of organizing the second contest in formal program verification for young engineers, researchers, and students from Russia. The contest was held in conjunction with the Workshop on Program Semantics, Specification, and Verification (PSSV) in Innopolis in October 2024. The contest format was close to the format of the so-called hackathons. Participants were asked to select and solve any of 5 verification problems using pre-defined model checking and deductive verification tools (Frama-C, Coq, C-lightVer, SPIN, TLC). We discuss the issues of organizing of the contest, the problems set, lessons learned from solutions submitted by contestants, and the overall feedback from the participants.
About the Authors
Dmitry Alexandrovich KONDRATYEV
Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences
Russian Federation
Russian Federation
– Cand. Sci. (Phys.-Math.), researcher at Ershov Institute of Informatics Systems Siberian Branch of the RAS, senior lecturer at Novosibirsk State University. Research interests: formal verification, deductive verification, Hoare logic and automated theorem proving.
Sergey Mikhailovich STAROLETOV
Polzunov Altai State Technical University
Russian Federation
Russian Federation
Cand. Sci. (Phys.-Math.), associate professor. Research interests: formal verification, model checking, cyber-physical systems, operating systems.
Irina Vladimirovna SHOSHMINA
Peter the Great St. Petersburg Polytechnic University
Russian Federation
Russian Federation
Cand. Sci. (Tech.), associate professor. Research interests: formal verification, model checking, distributed systems and algorithms.
Anastasiya Vladimirovna KRASNENKOVA
RusBITech-Astra
Russian Federation
Russian Federation
Security analyst at RusBITech-Astra. Research interests: formal verification, deductive verification, programming, security analysis, mathematical logic, distributed ledger systems.
Kirill Viktorovich ZIBOROV
Positive Technologies,
Lomonosov Moscow State University
Russian Federation
Russian Federation
Formal verification engineer at Positive Technologies, postgraduate student at Lomonosov Moscow State University. Research interests: formal verification, model checking, distributed systems and algorithms, distributed ledger systems.
Nikolay Vyacheslavovich SHILOV
Innopolis University
Russian Federation
Russian Federation
Cand. Sci. (Phys.-Math.), associate professor, head of the Laboratory of Software and Service Engineering of Innopolis University. Research interests: applied logic, foundations of Mathematics and Programming, Mathematical and Theory of Programming education and teaching
Natalia Olegovna GARANINA
Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences
Russian Federation
Russian Federation
Cand. Sci. (Phys.-Math.), senior researcher at Ershov Institute of Informatics Systems Siberian Branch of the RAS, associate professor at Novosibirsk State University. Research interests: formal verification, model checking, distributed systems, requirements engineering.
Timofey Yuryevich CHERGANOV
RusBITech-Astra
Russian Federation
Russian Federation
Senior security analyst at RusBITech-Astra. Research interests: formal verification, computer security.
References
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.
Review
For citations:
KONDRATYEV D.A., STAROLETOV S.M., SHOSHMINA I.V., KRASNENKOVA A.V., ZIBOROV K.V., SHILOV N.V., GARANINA N.O., CHERGANOV T.Yu. VeHa-2024 Formal Verification Contest: Two Years of Experience and Prospects. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(1):159-184. (In Russ.) https://doi.org/10.15514/ISPRAS-2025-37(1)-10
Email this article 