VeHa-2023 Formal Verification Contest: The Experience
Sergey Mikhailovich STAROLETOV,
Dmitry Alexandrovich KONDRATYEV,
Natalia Olegovna GARANINA,
Irina Vladimirovna SHOSHMINA https://doi.org/10.15514/ISPRAS-2024-36(2)-11
Abstract
To create modern competitive and trusted software, it is necessary to use knowledge of formal methods. Currently, a huge number of students are studying specialties related to programming. However, when studying at a university, it is difficult to gain the skill of practical application of theoretical knowledge. Short competitions with non-standard, industrial-related problems can arouse students' interest in the field of formal methods. The article describes the first experience of organizing a competition in formal verification of programs among students of Russian universities. The competition was held in conjunction with a seminar on program semantics, specification and verification (PSSV) in Innopolis in November 2023. The format of the competition was close to the format of so-called hackathons. Participants were asked to solve verification problems using predefined model checking and deductive verification tools. We consider the issues of organizing such an event, proposed tasks, results of decisions and feedback from participants.
About the Authors
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.
Dmitry Alexandrovich KONDRATYEV
Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences, Novosibirsk State University
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.
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.
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.
References
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.
Review
For citations:
STAROLETOV S.M., KONDRATYEV D.A., GARANINA N.O., SHOSHMINA I.V. VeHa-2023 Formal Verification Contest: The Experience. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2024;36(2):141-168. (In Russ.) https://doi.org/10.15514/ISPRAS-2024-36(2)-11
Email this article 