Сайт в процессе наполнения. Архив всех прошедших курсов доступен на старой версии сайта по адресу old.compsciclub.ru
Город: Санкт-Петербург Казань Язык: Русский English

Введение в моделирование и верификацию аппаратных и программных систем
Осень 2007, посмотреть все семестры

Запишитесь на курс, чтобы получать уведомления и иметь возможность сдавать домашние задания. Для записи требуется регистрация на сайте.
Перейти к регистрации Войти

Верификация — это проверка того, что аппаратная или программная система соответствует заявленной спецификации (то есть обладает необходимыми свойствами). Данный курс является введением в методы верификации аппаратных и программных систем. В частности, будут освещены следующие темы:

  • реактивные системы и их моделирование;
  • временные логики;
  • метод проверки моделей (model checking) и алгоритмы для проверки моделей;
  • задача булевой выполнимости и ее роль в верификации аппаратных и программных систем.

Наряду с теоретическими основами верификации будут рассмотрены программные средства для верификации и примеры.

Дата и время Название Место Материалы
20 октября
17:00–18:30
Введение, лекция ПОМИ РАН слайды
20 октября
18:40–20:10
Системы переходов для моделирования систем, лекция ПОМИ РАН слайды
21 октября
17:15–18:45
Логика линейного времени, лекция ПОМИ РАН слайды
21 октября
19:00–20:30
Дедуктивная LTL верификация, лекция ПОМИ РАН слайды
21 октября
19:00–20:30
Логика деревьев вычислений CTL, лекция ПОМИ РАН слайды
21 октября
20:30–22:00
Двоичные разрешающие диаграммы (BDD). Символьная проверка моделей, лекция ПОМИ РАН слайды
21 октября
20:30–22:00
Проверка моделей на практике, лекция ПОМИ РАН слайды
03 ноября
17:25–18:55
Представление с неподвижной точкой. Условия справедливости. Синтез OBDD, лекция ПОМИ РАН слайды
03 ноября
17:25–18:55
Разделенная нормальная форма для логики линейного времени LTL: определение и приведение к разделенной нормальной форме с условными обязательствами, лекция ПОМИ РАН слайды
04 ноября
17:30–19:00
Проверка моделей ограниченной глубины, лекция ПОМИ РАН слайды
04 ноября
17:30–19:00
Автоматный подход, лекция ПОМИ РАН слайды
04 ноября
17:30–19:00
Разделенная нормальная форма для логики линейного времени LTL: условные обязательства и построение автомата, лекция ПОМИ РАН слайды
04 ноября
19:15–20:45
Свидетельства и контрпримеры. Абстракция, лекция ПОМИ РАН слайды
04 ноября
19:15–20:45
Заключение и чего же ожидать в экзамене, лекция ПОМИ РАН слайды