Контест VeHa

Задача 1. Верификация функции проверки прав доступа на Frama-C

Команда 1 (Когтенков А.В.) — Благодарность

Buffer_Overflow — Диплом за I место (10 баллов)

re_tofl — Диплом за II место (8 баллов)

DevTools_Itmo — Почётная грамота за успешное освоение инструмента Frama-C (6 баллов)

Комментарии экспертов тут.

Задача 2. Верификация функции проверки прав доступа на Coq

Диплом I: Алексей Волков (МФТИ, VK Tech), Глеб (ООО), Иван Смирнов (МФТИ), orenty7 (отсутствует)

Диплом II: 1 (частное лицо)

Грамоты и призы:

• Алексей Волков — за самое быстрое решение

• Глеб — за внимание к корректности функциональной спецификации

• Иван Смирнов — за самое короткое решение и использование автоматики

• orenty7 — за выделение вспомогательных утверждений.

Задача 3. Моделирование вычислительного pipeline GPU с поиском оптимальных параметров с помощью Model Checking

RARe -- Диплом за I место (42 балла за уровни 1 и 2). Предупреждение за неспортивное поведение (решение уровня 3 аннулировано)

Power O` Nine — Диплом за II место (38 баллов за уровни 1-3)

Power O` Nine — Дополнительно почетная грамота "За найденную ошибку в исходном коде"

Комментарии экспертов тут.

Задача 4. Дедуктивная верификация программы, относящейся к задаче проверки выполнимости булевых формул (SAT)

1: Когтенков Александр Валентинович — Благодарственное письмо за лучшее решение задач соревнования VeHa-2024

Шутова Мария Андреевна (СПбПУ) — 

• Диплом I степени 

• Почетная грамота за волю к победе

Панченко Наталья Андреевна НГУ — Диплом I степени

VeriFLOWers: Малиновский Денис Владимирович, Чумак Антон Максимович, Гунько Тимур Витальевич (НГУ) — Диплом I степени 

Point: Егоров Анатолий Романович, Еремина Ксения Игоревна (СПбПУ) — Диплом I степени  

Главные критерии для выбора наград участникам соревнования следующие: правильно ли задан инвариант цикла и позволяет ли заданный инвариант цикла провести автоматическую успешную верификацию программы в программной системе C-lightVer.

Задача 5. Построение и проверка модели протокола консенсуса IBFT

Победители не определены.

О вручении

• В начале ноября определимся по текстам грамот и людям (фамилии, университеты) исходя из данных о регистрации

• Вручение дипломов и грамот в Москве планируется на ИСП РАН Open (начало декабря), в Новосибирске и Петербурге - на "подобающем" семинаре предположительно в декабре

• Всем дипломантам и отмеченным грамотами — мерчи от Университета Иннополис (какие - уточняется), призы по номинациям от компаний Astra и PT.