Миссия данного сайта - облегчить страдания студентов МФТИ и ВШЭ при прохождении курса "Формальная верификация" в ИСП РАН.
Состав курса
- Практикум по frama-c
- Практикум по spin
-
Контрольная работа 1
- Метод Флойда
- Построение КНФ по кодировке Цейтина
- Разрешающая процедура Нельсона-Оппена
-
Контрольная работа 2
- Построение LTL
- Преобразование LTL → Автомат Бюхи
- Построение ROBDD
- Дополнительный практикум по алгоритму DPLL
- Дополнительный практикум по преобразованию LTL в автомат Бюхи
Для закрытия курса минимально необходимо сдать (читай получить любую оценку) два обязательных практикума и написать две контрольные работы. Без учета дополнительных заданий потолок оценки составит хор(6). Для повышения потолка надо сдавать доп. задания.
Автоматические солверы
Большинство задач на контрольных решаются алгоритмически, но требуют значительных затрат по времени и большой внимательности. В связи с этим были написаны автоматические солверы. Они доступны в верхнем меню и в составе курса.
База знаний
Помимо солверов на данном сайте имеется база знаний, включающая в себя все, что удалось собрать для упрощения жизни:
Важная информация
Стоит отметить, что каждый год могут предъявляться новые требования к сдаче заданий, а также могут быть созданы новые варианты практикумов/задач. Не стоит бездумно полагаться на этот сайт, он (наверное) может налажать в решении задач.
В целом, если что-то на сайте лагает, некорректно работает или неправильно решает задачу, создавайте issue в репозитории проекта (ссылка на репозиторий присутствует в подвале), мы постараемся решить эти проблемы максимально оперативно.