Формальные методы в программной инженерии

 

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

Вопросы по курсу можно задавать на форуме http://forum.oberoncore.ru/viewtopic.php?f=140&t=5915

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

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

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

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

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

Лекция: SMT-решатели, 2017

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

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

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

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

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

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

Лекция 2.2

Лекция 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

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

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

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

Лекция 3. Стандартная библиотека системы Why3

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

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

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

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