Список всех тем лекций
Лекция 1. Верификация программ. Метод Флойда.
Введение
Вычисление квадрата натурального числа
Вычисление целой части корня неотрицательного числа
Возведение числа в степень
Лекция 2. Верификация программ (продолжение). Сортировка пузырьком.
Массивы
Сортировка массива
Блок-схема для сортировки пузырьком
Проверка корректности
Проверка завершаемости
Лекция 3. Функциональные программы.
Базовые функции
Сложные функции
О функциональных программах
Функция Фибоначчи
Программа сортировки
Леммы
Лекция 4. Параллельные и распределенные программы.
Введение
Процессная нотация (другое определение программы)
Гонки
Задача о вычислении k! с помощью двух процессов
Проверка корректности
Верификация параллельной программы методом Флойда
Программа сортировки массива длины n на n процессорах
MPI
Перемножение матриц (упражнение)
Посылка и прием сообщений со значениями в MPI
Избрание лидера (упражнение)
Лекция 5. Неподвижные точки функциональных программ.
Введение
Функциональная программа (повторение)
Работа с функциональной программой
Неопределенное значение
Естественное расширение функций
Частично упорядоченные множества и кортежи
Пример немонотонной функции
Ее монотонность
Неподвижная точка
Функциональные программы с разным количеством решений
Существование sup у цепи кортежей
Пример монотонного функционала, не являющегося непрерывным
Теорема Тарского (существование наименьшей неподвижной точки)
Вопрос о вычислении неподвижной точки на конкретном аргументе
Лекция 6. Существование наименьшей неподвижной точки. Вычисление значения неподвижной точки на конкретных данных.
Повторение
Монотонность функционала
Непрерывность функционала
Существование наименьшей неподвижной точки
Понятие компиляции
Вычисление неподвижной точки на конкретных данных
Пример аномалии при использовании немонотонной функции
Лекция 7. Верификация распределенных систем. Задача вычисления произведения матриц.
Комплексы взаимодействующих последовательных программ
Передача сообщений с помощью каналов и общих переменных
Задача вычисления произведения матриц
Процесс-менеджер
Процесс-работник
Возможные дополнительные условия
Введение дополнительных переменных
Теорема
Лекция 8. Пример верификации распределенной программы (умножение двух матриц).
Устройство распределенной программы для умножения двух матриц (повторение)
Теорема (свойства)
Доказательство теоремы
Завершение программы за конечное число шагов
Лекция 9. Теория процессов. Понятие процесса. Операции над процессами. Эквивалентность процессов.
Введение в теорию процессов
Пример с торговым автоматом
Операции на процессах
Сильная эквивалентность процессов
Лекция 10. Бимоделирование. Критерий сильной эквивалентности процессов. Наблюдаемая эквивалентность.
Эквивалентность процессов (повторение)
Сильное отношение эквивалентности (продолжение доказательства)
Пример для процесса, вычисляющего x*x
Бимоделирование
Теорема о связи сильной эквивалентности процессов и бимоделирования между ними
Конгруэнция
Алгоритм доказательства эквивалентности двух процессов
Задача минимизации процессов по числу состояний
Домашнее задание
Наблюдаемая эквивалентность
Лекция 11. Наблюдаемая эквивалентность. Планировщик процессов (пример).
Наблюдаемая эквивалентность процессов
Постановка задачи и планы на следующую лекцию
Другое определение наблюдаемой эквивалентности процессов
О свойствах наблюдаемой эквивалентности (по аналогии с сильной эквивалентностью)
Планировщик для операционной системы (пример)
Представление работы планировщика с помощью циклеров
Формальное доказательство свойства (последовательность действий, генерируемых планировщиком и обозначенных альфа, является правильной циклической последовательностью)
Схема дальнейшего доказательства
Модификация задачи
Лекция 12. Формальная модель криптографических протоколов. Протокол Yaholom.
Вступление
Протокол Yaholom
Формальная модель криптографического протокола
Постановка задачи
Семинар 1. Введение в Isabelle. Лямбда-исчисление.
Формальная верификация
Пример
Isabelle
Работа с Isabelle (код)
Лямбда-исчисление
Бета-редукция
Свободные и связанные переменные
Равенство лямбда-термов
Нумералы Чёрча
Парадокс Рассела
Семинар 2. Лямбда-исчисление (продолжение). Доказательства в Isabelle.
Типизация по Чёрчу и по Карри
Полнота по Тьюрингу
Реализация в Isabelle (код)
Реализация в Isabelle (код)
Унификация в Isabelle (теория и код)
Примеры (теория и код)
Безопасные и небезопасные правила
Разбор упражнения (код)
Семинар 3. Логика первого порядка. Методы автоматизации доказательств.
Правила для кванторов
Атрибуты of и where
Доказательство прямым выводом (forward proof)
Атрибуты OF и THEN
Настройка с помощью атрибутов
Упражнение
Семинар 4. Логика высшего порядка Isabelle/HOL.
Семинар 5. Переписывание термов. Симплификатор Isabelle.
Пример завершаемой системы
Атрибуты симплификатора
Приписывание assumption
Более сложный пример доказательства
Другие методы автоматизации (примеры доказательств)
Примеры (код)
Разбиение на случаи
Правила конгруэнции
Упорядоченное переписывание
Отладка симплификаторов
Семинар 6. Объявление типов в Isabelle/HOL. Рекурсивные функции. Индукция.
Семинар 7. Индуктивные отношения. Язык структурированных доказательств Isar.
Ключевое слово inductive_set
Примеры (код)
Синтаксис
Примеры (код)
Шаблоны доказательств (теория и код)
Семинар 8. Язык структурированных доказательств Isar (продолжение).
Представление теоремы на языке Isar (повторение)
Синтаксис для локальных лемм (повторение)
Пример
Теорема про квадрат разности (пример)
(пример)
Метод cases
Структурная индукция
Вычислительная индукция (пример)
Семинар 9. Механизм локалей в Isabelle. Примеры практического применения инструмента.
Синтаксис локалей
Дополнение локали
Импорт локалей
Команда sublocale
Команда interpret
Верификация алгоритма stablecoin
Верификация функционального алгоритма сортировки вставками
