Участники решали задачи по верификации моделей и дедуктивной верификации с тьюториалами. Контест прошёл онлайн в рамках ежегодного семинара Program Semantics, Specification and Verification, организованного Университетом Иннополис.

Задача по верификации моделей заключалась в превращении программы на формальном языке в систему переходов и проверке её свойств с использованием темпоральных формул. В направлении дедуктивной верификации участникам предстояло проверить правильность программы относительно её формальной спецификации с помощью системы логических правил вывода.

1 и 2 место заняли команды студентов Санкт-Петербургского политехнического университета Петра Великого, 3 место — команда Новосибирского государственного университета.

Организаторы соревнования — специалисты Университета Иннополис, НГУ, СПбГТУ и АлтГТУ.

Подробнее о контесте: sites.google.com/view/veha23

Подробнее о семинаре: persons.iis.nsk.su/en/PSSVfrom2022towards2023