City: Saint Petersburg Novosibirsk Kazan Language: Русский English

Introduction to Verification
Saint Petersburg / autumn 2007, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

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

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

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

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