Д. А. Кондратьев, С. М. Старолетов, И. В. Шошмина, А. В. Красненкова, К. В. Зиборов, Н. В. Шилов, Н. О. Гаранина, Т. Ю. Черганов, “Соревнования по формальной верификации VeHa-2024: накопленный в течение двух лет опыт и перспективы”, Труды ИСП РАН, 2025, том 37, выпуск 1,страницы 159

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

Д. А. Кондратьев^a, С. М. Старолетов^b, И. В. Шошмина^c, А. В. Красненкова^d, К. В. Зиборов^ef, Н. В. Шилов^g, Н. О. Гаранина^a, Т. Ю. Черганов^d

^a Институт систем информатики им. А. П. Ершова СО РАН
^b Алтайский государственный технический университет им. И. И. Ползунова
^c Санкт-Петербургский политехнический университет Петра Великого
^d РусБИТех-Астра
^e Positive Technologies
^f Московский государственный университет имени М. В. Ломоносова
^g Университет Иннополис

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

Ключевые слова: формальные методы, соревнования по формальной верификации, проверка моделей, дедуктивная верификация, хакатон

DOI: 10.15514/ISPRAS-2025-37(1)-10