Задачи контеста
Задача о станции "Луна-25" (Model checking)
Уровень: начальный
Цель: на языке Promela формализовать взаимодействие модулей станции и найти сценарий, приводящий к ошибке, описанной в СМИ
Задачу предложили: Гаранина, Шошмина
Моделирование pipeline GPGPU (Model checking)
Уровень: сложный
Цель: Описать pipeline процессов, происходящих в GPU при решении задачи на SIMT-ядрах согласно известным публикациям
Задачу предложили: Старолетов, Гаранина
Описание протокола телеграмм для европоездов (Model checking)
Уровень: сложный
Цель: Реализовать алгоритм работы с бинарными сообщениями согласно официальному документу и проверить корректность кодирования/декодирования
Задачу предложил: Старолетов
Задача по дедуктивной верификации программы, предназначенной для решения такой проблемы миссии "Луна-25", как проверка равенства всех приоритетов в массиве команд
Уровень: средний
Цель: задать формальные спецификации программы, предназначенной для решения такой проблемы миссии "Луна-25", как проверка равенства всех приоритетов в массиве команд, и провести автоматическую дедуктивную верификацию данной программы в системе C-lightVer
Задачу предложил: Кондратьев