Proceedings of the Institute for System Programming of the RAS
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS


Proceedings of ISP RAS:
Year:
Volume:
Issue:
Page:
Find




Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register

Proceedings of the Institute for System Programming of the RAS, 2025, Volume 37, Issue 1, Pages 159–184
DOI: https://doi.org/10.15514/ISPRAS-2025-37(1)-10 (Mi tisp958) 		 
VeHa-2024 formal verification contest: two years of experience and prospects

D. A. Kondrat'eva, S. M. Staroletovb, I. V. Shoshminac, A. V. Krasnenkovad, K. V. Ziborovef, N. V. Shilovg, N. O. Garaninaa, T. Yu. Cherganovd

a A.P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences
b Altai State Technical University
c Peter the Great St. Petersburg Polytechnic University
d RusBITech-Astra
e Positive Technologies
f Lomonosov Moscow State University
g Innopolis University
Full-text PDF (1328 kB)
DOI: 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.
Keywords: formal methods, formal verification competitions, model checking, deductive verification, hackathon
Document Type: Article
Language: Russian
Citation: D. A. Kondrat'ev, S. M. Staroletov, I. V. Shoshmina, A. V. Krasnenkova, K. V. Ziborov, N. V. Shilov, N. O. Garanina, T. Yu. Cherganov, “VeHa-2024 formal verification contest: two years of experience and prospects”, Proceedings of ISP RAS, 37:1 (2025), 159–184
Citation in format AMSBIB
\Bibitem{KonStaSho25}
\by D.~A.~Kondrat'ev, S.~M.~Staroletov, I.~V.~Shoshmina, A.~V.~Krasnenkova, K.~V.~Ziborov, N.~V.~Shilov, N.~O.~Garanina, T.~Yu.~Cherganov
\paper VeHa-2024 formal verification contest: two years of experience and prospects
\jour Proceedings of ISP RAS
\yr 2025
\vol 37
\issue 1
\pages 159--184
\mathnet{http://mi.mathnet.ru/tisp958}
Linking options:
  • https://www.mathnet.ru/eng/tisp958
  • https://www.mathnet.ru/eng/tisp/v37/i1/p159
    • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    		Proceedings of the Institute for System Programming of the RAS
    Statistics & downloads:
    Abstract page:73
    Full-text PDF :44
     
      Contact us:
    		  Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2026