PowerPoint и PDF презентации лекций

Презентации иногда полезно просматривать параллельно с прослушиванием лекций. Из презентаций удобнее получить доступ к учебным материалам, представленных Интернет-ссылками.

Общее введение по курсу «Формальные методы»

Раздел 1. SMT-решатели

Лекция 1: Задачи SAT и SMT

Лекция 2: Обзор языка SMT-LIB

Лекция 2018г.: SMT-решатели

Практическое занятие

Раздел 2. Спецификация и верификация программ в предикатном и автоматном программировании

Введение по разделу 2

Лекция 1: Основы. Класс программ-функций

Лекция 2: Формальная семантика языка предикатного программирования

Лекция 3: Построение языка предикатного программирования

Лекция 4: Метод предикатного программирования

Лекция 5: Гиперфункции

Практическое занятие 1 на построение формальных спецификаций

Лекция 6: Дедуктивная верификация. Программный синтез. Язык спецификаций PVS

Лекция 7: Система PVS: библиотеки теорий. Блок доказательства

Лекция 8: Автоматное программирование. Основы

Лекция 9: Автоматное программирование. Примеры

Практическое задание 2 Техника доказательства в системе PVS

Раздел 3. Верификация программных систем методом проверки моделей

Лекция 1: Введение

Лекция 2: Проверка моделей

Лекция 3: Логики CTL, LTL

Лекция 4: Проверка на модели для CTL и  LTL

Лекция 5: Символьные представления

Раздел 4. Язык спецификаций и методы автоматического доказательства в системе Why3

Введение по разделу 4

Лекция 1. Архитектура и язык системы Why3

Лекция 2. Язык функционального программирования WhyML

Лекция 4. Трансформации системы Why3

Лекция 5. Доказательство в системе Why3

Раздел 4. Методы спецификации и анализа терминологических систем

Введение по разделу 4