III Контест VeHa

Результаты VeHa-2025 🎉 

Задача 1 (Моделирование и предотвращение катастрофы китайских скоростных поездов методом Model Checking): 

Одна команда подала решение. Но катастрофа в решении не была промоделирована полностью.

Команда T1 -- диплом 🏅 "За успешное моделирование системы управления поездами и ознакомление со средством верификации SPIN".

Задача 2 (TLA+: Temporal Logic of Actions + data structures):

🥇1 место -- команда NeVer

🥈2 место -- команда Pleshcheyevo ozero surf club🏄

🥈2 место -- команда MNeyzov

🥉3 место -- команда Osichiki

4 место -- команда VeryVerifiers

4 место -- команда SmirnovIN

5 место -- команда verifly

Подробнее о результатах

Задача 3 (Пошаговое выведение свойств в Isabelle/HOL): 

🥇1 место -- команда ChernenkoI

🥈2 место -- команда IFTHENFI

🥈2 место -- команда Axiomatic

🥉3 место -- команда VeryVerifiers

4 место -- команда SPbPU-40202

5 место -- команда ISP RAS

6 место -- команда BufferOverflow

7 место -- команда AlKhakov‘s team

Подробнее о результатах Дополнительный опрос по номинации

Задача 4 (Дедуктивная верификация с использованием Rocq):

Три команды предоставили решения. Победитель в номинации -- команда Cache Invalidation🥇. 

Команды Gaba🏅 и Pleshcheyevo ozero surf club🏅 награждаются грамотами за решение задач соревнования. Готовы призы для всех участников команд 🎁 (6 человек). Репозиторий с решениями и результатами

Задача 5 (Дедуктивная верификация решающей квадратичное диофантово уравнение Пелля программы, реализующей разработанный в Индии метод «чакравала», являющийся одним из первых в истории математики циклическим алгоритмом):

Диплом I степени🥇 -- команда SPbPU-40202

Диплом II степени🥈 + Почетная грамота за анализ достижимости и завершимости программного кода🏅-- команда Degraded Zebra

Дополнительные сведения

Задача 6 (Дедуктивная верификация эффективной программы поиска по строке):

🥇1 место -- команда Vitaly (10 баллов)

🥈2 место -- команда VeryVerifier (9 баллов)

🥉3 место -- команда SmirnovIN (7 баллов)

4 место -- Команда BuferOverflow (3 балла)

Дополнительные сведения

Спасибо за участие!

Планируются дипломы и призы от компаний и из фонда В.А. Непомнящего. Подробнее данные о награждении будут опубликованы здесь и в телеграмм-канале!

Телеграм-канал мероприятия: Contest VeHa

Соревнования будут проводиться в системе тестирования NSU-TS

Трёхдневное мероприятие в рамках XXVI Открытой Всесибирской олимпиады по программированию им. И.В. Поттосина, в ходе которого можно будет познакомиться с инструментами формальной верификации и порешать интересные задачи

 Направления