Developing highly reliable software requires the use of formal verification methods, but integrating them into the education of IT students is difficult due to the gap between theoretical understanding and practical skills. In this paper, we present the design, implementation, and analysis of VeHa-2025, a national verification hackathon aimed at overcoming these challenges through hands-on learning, particularly through competitions focused on specific verification problems. Our event combines tracks in model checking (SPIN, TLA+) and deductive verification (Isabelle/HOL, Coq-Rocq, Why3, C-lightVer). Launched in 2023 as a volunteer initiative by a group of academics, VeHa evolved into an academy-industry partnership by 2025. VeHa-2025 included a structured educational cycle consisting of preparatory workshops, an invited lecture, a three-day competitive problem-solving period, and a post-event verification of solutions. The analysis of metrics, submitted solutions, and participant feedback presented in this article demonstrates the growing effectiveness of our hackathon in developing practical skills, building a community, and equipping participants with competencies in formal methods that are in demand in industry. We argue that such competitive, practice-oriented formats are a valuable pedagogical tool for motivating and training the next generation of software verification engineers.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education

  • Sergey Staroletov,
  • Dmitry Kondratyev,
  • Vladimir Shelekhov,
  • Alexander Kogtenkov,
  • Nikolay V. Shilov,
  • Natalia Garanina,
  • Irina Shoshmina,
  • Timofey Cherganov,
  • Vasil Dyadov

摘要

Developing highly reliable software requires the use of formal verification methods, but integrating them into the education of IT students is difficult due to the gap between theoretical understanding and practical skills. In this paper, we present the design, implementation, and analysis of VeHa-2025, a national verification hackathon aimed at overcoming these challenges through hands-on learning, particularly through competitions focused on specific verification problems. Our event combines tracks in model checking (SPIN, TLA+) and deductive verification (Isabelle/HOL, Coq-Rocq, Why3, C-lightVer). Launched in 2023 as a volunteer initiative by a group of academics, VeHa evolved into an academy-industry partnership by 2025. VeHa-2025 included a structured educational cycle consisting of preparatory workshops, an invited lecture, a three-day competitive problem-solving period, and a post-event verification of solutions. The analysis of metrics, submitted solutions, and participant feedback presented in this article demonstrates the growing effectiveness of our hackathon in developing practical skills, building a community, and equipping participants with competencies in formal methods that are in demand in industry. We argue that such competitive, practice-oriented formats are a valuable pedagogical tool for motivating and training the next generation of software verification engineers.