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