Команды НГУ стали призерами третьего всероссийского соревнования по формальной верификации программ VeHa-2025

Третье всероссийское соревнование по формальной верификации программ VeHa-2025 прошло 4–8 ноября, оно стало мероприятием-спутником XXVI Открытой Всесибирской олимпиады по программированию им. И. В. Поттосина. В соревнованиях приняли участие представители ведущих российских компаний, университетов и научных институтов.

Задачи соревнования были посвящены проверке корректности программных систем — от алгоритмов решения диофантовых уравнений индийским методом «чакравала» и поиска подстроки в строке текста до моделей управления китайскими высокоскоростными поездами и статического анализа программ. Участники должны были погрузиться в выбранную область и доказать корректность алгоритмов с применением методов формальной верификации. В организации соревнования VeHa-2025 принимали участие сотрудники кафедры программирования Механико-математического факультета НГУ и сотрудники кафедры систем информатики Факультета информационных технологий НГУ: Дмитрий Кондратьев, Наталья Гаранина и Владимир Шелехов.

В VeHa-2025 участвовали команды из Новосибирского государственного университета, Группы Астра, Лаборатории Касперского, Института системного программирования им. В.П. Иванникова РАН, Математического института им. В. А. Стеклова РАН, Санкт-Петербургского политехнического университета Петра Великого, МГТУ им. Н. Э. Баумана, Университета Неаполис Пафос, Московского физико-технического института, Университета ИТМО, Университета МИСИС и Института автоматики и электрометрии СО РАН.

Команды НГУ показали высокие результаты. В номинации «Пошаговое выведение свойств в Isabelle/HOL» (Лаборатория Касперского) второе место разделили:

— аспирант Факультета информационных технологий (ФИТ) Артём Ищенко,

— студент 3 курса Механико-математического факультета (ММФ) Лев Бояндин.

Первое место занял выпускник ФИТ, ныне аспирант ИАиЭ, Иван Черненко.

— Я интересуюсь формальными методами и системами интерактивного доказательства теорем, поэтому тематика соревнования оказалась мне очень близка. Участвовал заочно, вопросы обсуждал с ментором в общей беседе. Из-за загруженности выбрал только одну номинацию — по Isabelle/HOL. Пара моментов были сложными, но в целом всё шло гладко. Уровнем сложности остался доволен. Очень рад занять призовое место, — рассказал Лев Бояндин.

Отдельно отметилась команда студентки 4 курса ФИТ Маргариты Шабановой — она стала единственным номинантом задачи, максимально приближённой к реальной индустриальной постановке, связанной с моделированием системы управления китайскими скоростными поездами. В соревновании также участвовали студент ММФ Александр Харьков и магистрант ММФ Юлия Разбитнова.

— Тематика олимпиады совпадает с направлением моей дипломной работы, и мне хотелось получить навыки, которые пригодятся дальше, а также расширить кругозор. Было интересно попробовать силы в задачах, выходящих за рамки учебной программы. Соревнования прошли очень динамично: за ограниченное время нужно было быстро понимать условие и продумывать решение. Атмосфера была рабочей, но дружелюбной — организаторы оперативно отвечали на вопросы, — поделилась впечатлениями Маргарита Шабанова.

Поздравляем участников и желаем им дальнейших успехов в исследовательской и проектной деятельности!

Материал подготовили Дмитрий Кондратьев, Наталья Гаранина и Владимир Шелехов.

Источники:

Команды НГУ стали призерами третьего всероссийского соревнования по формальной верификации программ VeHa-2025 – Новосибирский государственный университет (nsu.ru), Новосибирск, 24 ноября 2025.