Общее введение по курсу «Формальные методы»:
Вопросы по курсу можно задавать на форуме http://forum.oberoncore.ru/viewtopic.php?f=140&t=5915
PowerPoint и PDF презентации лекций
Раздел 1. SMT-решатели
Лекция 1: Задачи SAT и SMT, 2016
Лекция 2: Обзор SMT-LIB, 2016
Лекция: SMT-решатели, 2017
Раздел 2. Спецификация и верификация программ в предикатном и автоматном программировании
Лекция 1: Основные понятия. Класс программ-функций
Лекция 2: Формальная семантика языка предикатного программирования (2018)
Лекция 2.1: Формальная семантика языка предикатного программирования (2017)
Лекция 3: Построение языка предикатного программирования (2018)
Лекция 3: Построение языка предикатного программирования (2016)
Лекция 4.1: Метод предикатного программирования
Лекция 4.2: Оптимизирующие трансформации предикатных программ
Лекция 5: Гиперфункции
Лекция 6: Дедуктивная верификация. Программный синтез. Язык спецификаций PVS
Практическое занятие 1 на построение спецификации
Лекция 7: Система команд PVS. Практика работы с PVS
Лекция 8: Автоматное программирование. Основы
Лекция 9: Автоматное программирование. Примеры
Практическое задание 2 Техника доказательства в системе PVS
Раздел 3. Верификация программных систем методом проверки моделей
Лекция 1: Введение
Лекция 2: Структура Крипке. Представление программных систем
Лекция 3: Темпоральные логики LTL и CTL
Лекция 4.1: Проверка моделей для LTL
Лекция 4.2: Проверка моделей для CTL
Лекция 5: Символьный алгоритм проверки на модели
Практическое задание 2. Построение модели и проверка ее свойств
Практическое занятие 3. Система верификации Spin. Язык Promela.
Лекция 6: Алгоритм Чанди-Лампорта
Раздел 4. Язык спецификаций и методы автоматического доказательства в системе Why3
Лекция 1. Архитектура и язык системы Why3
Лекция 2. Язык функционального программирования WhyML
Лекция 3. Стандартная библиотека системы Why3
Лекция 4. Трансформации системы Why3
Лекция 5. Доказательство в системе Why3
Раздел 5. Методы спецификации и анализа терминологических систем