Соревнования по формальной верификации VeHa-2023: опыт проведения

Для создания современного конкурентоспособного и доверенного программного обеспечения необходимо использовать знания формальных методов. В настоящее время огромное количество студентов обучается специальностям, связанным с программированием. Однако при обучении в вузе сложно получить навык практического применения теоретических знаний. Короткие соревнования с нестандартными близкими к промышленным задачами могут пробудить интерес студентов к области формальных методов. В нашей статье описан первый опыт организации соревнования по формальной верификации программ среди студентов российских вузов. Соревнования проводились в связке с семинаром по семантике, спецификации и верификации программ (PSSV) в Иннополисе в ноябре 2023 года. Формат соревнования был близок к формату так называемых хакатонов. Участникам было предложено решить задачи по верификации с использованием заранее определенных инструментов проверки моделей и дедуктивной верификации. Мы рассмотрим вопросы организации такого мероприятия, предложенные задачи, результаты решений и обратную связь от участников.