В конце октября прошло Второе всероссийское соревнование по формальной верификации программы VeHa-2024. Оно состоялось в рамках конференции PSSV-2024. Организаторы и участники соревнования VeHa-2024 представляли известные российские компании, университеты и научные институты. В числе организаторов и судей соревнования VeHa-2024 были сотрудники кафедры программирования Механико-математического факультета НГУ и преподаватели профиля «Формальные методы анализа программ и систем» Наталья Гаранина и Дмитрий Кондратьев.
Cоревнование включало в себя задачи по основным направлениям формальной верификации программ, таким как дедуктивная верификация и проверка на модели. Победителями и призерами соревнования VeHa-2024 в различных номинациях стали студенты из Новосибирского государственного университета, Санкт-Петербургского политехнического университета Петра Великого, Московского физико-технического института и Университета ИТМО.
Команды Механико-математического факультета и Факультета информационных технологий НГУ стали победителями в номинации «Дедуктивная верификация программы, относящейся к задаче проверки выполнимости булевых формул (SAT)». Команду ММФ представляла Наталья Панченко (2 курс магистратуры, «Формальные методы анализа программ и систем»), дополнившая свое призовое место на прошлогоднем соревновании VeHa победой в этом году. В состав команды ФИТ вошли Денис Малиновский, Артем Чумак и Тимур Гунько (3 курс).
Участники соревнования отметили, что задачи были не просто сложны, но и максимально практикоориентированы. Например, проверка корректности SAT-решателей, прав доступа к операционному оборудованию и моделям графических процессоров требует глубокого понимания теории и методов их применения в реальной жизни.
— Мы решили участвовать в хакатоне VeHa-2024, так как хотели попробовать себя в чём-то новом, применив на практике знания, полученные за курсы математической логики и МТК (методы трансляции и компиляции). Соревнования проходили в течение трёх дней, и за это время нам предстояло решить задачу по дедуктивной верификация программы, относящейся к задаче проверки выполнимости булевых формул. Мы разделили решение задачи на несколько этапов. Первый — внимательное самостоятельное изучение условия задачи, знакомство с теорией, а также изучение языка Lisp, на котором предстояло писать решение. Второй — встреча и обсуждение полученных вследствие самостоятельной работы знаний, разрешение всех моментов недопонимания и пробелов и последующее их приведение к общему знаменателю. Третий —обсуждение и выработка вариантов решения задачи. Четвертый — написание решения и его последующее тестирование. Благодаря такому организованному подходу мы смогли довольно быстро разобраться со всеми проблемами и занять первое место, — рассказывает Денис Малиновский.
Задачи соревнования были связаны с проверкой корректности программных систем для обеспечения их надежности, в том числе SAT-решателей, играющих важную роль в области автоматического доказательства теорем, модуля проверки прав доступа в операционных системах, моделей коммуникационных протоколов и моделей графического процессора. Участники соревнования смогли изучить как минимум одну из этих сложных областей и попробовать свои силы в доказательстве корректности соответствующей системы с помощью методов формальной верификации программ.Материалы соревнования размещены на сайте VeHa-2024.
— В начале соревнования мы вместе пробовали решать, но поняли, что нам нужно ещё изучить теорию, а уже после этого каждый из нас понемногу дополнял то, что мы написали на старте. Лично мне было трудно влиться в процесс, так как с подобными соревнованиями до этого не сталкивался. Но ощущения у меня приятные. Понравилось, что успешно изучили что-то новое, — поделился эмоциями Тимур Гунько.
Такие конкурсы направлены на развитие инженерного мышления, повышение уровня подготовки студентов и помогают им лучше понять, как теория превращается в эффективные инструменты для обеспечения надежности программных систем.
