Embedded Files
На данном соревновании победители будут объявлены по каждой номинации👇
1. Верификация функции проверки прав доступа на Frama-C
1. Верификация функции проверки прав доступа на Frama-C
Уровень: средний
Цель: формальная верификация одной из функций модуля безопасности ядра Linux с помощью Frama-C.
Задачу предложили: А. Кокорин, А. Красненкова
2. Верификация функции проверки прав доступа на Coq
2. Верификация функции проверки прав доступа на Coq
Уровень: сложный
Цель: Цель: формальная верификация одной из функций модуля безопасности ядра Linux с помощью Coq.
Задачу предложил: Т. Черганов
3. Моделирование вычислительного pipeline GPU с поиском оптимальных параметров с помощью Model Checking
3. Моделирование вычислительного pipeline GPU с поиском оптимальных параметров с помощью Model Checking
Уровень: средний/сложный
Цель: Смоделировать работу GPU при решении параллельной задачи на SIMT-ядрах с поиском оптимальных параметров методом Model Checking
Задачу предложили: Шошмина, Старолетов, Гаранина
4. Дедуктивная верификация программы, относящейся к задаче проверки выполнимости булевых формул (SAT)
4. Дедуктивная верификация программы, относящейся к задаче проверки выполнимости булевых формул (SAT)
Уровень: средний
Цель: Дедуктивно проверить C-код для задачи SAT
Задание twosat_solver.c twosat-solver.lisp
Задачу предложил: Д. Кондратьев
5. Построение и проверка модели протокола консенсуса IBFT
5. Построение и проверка модели протокола консенсуса IBFT
Page updated
Google Sites
Report abuse