Формальная семантика и верификация программного обеспечения
Математика
21 лекция
2023
лекции
спецкурс
Механико-математический факультет
Математика
спецкурс
Преподаватель
- 01:31:45Лекция 1. Верификация программ. Метод Флойда
- 01:12:47Семинар 1. Введение в Isabelle. Лямбда-исчисление
- 01:23:52Лекция 2. Верификация программ (продолжение). Сортировка пузырьком
- 01:21:28Семинар 2. Лямбда-исчисление (продолжение). Доказательства в Isabelle
- 01:15:12Лекция 3. Функциональные программы
- 01:02:16Семинар 3. Логика первого порядка. Методы автоматизации доказательств
- 01:21:43Лекция 4. Параллельные и распределенные программы
- 50:40Семинар 4. Логика высшего порядка Isabelle/HOL
- 01:28:28Лекция 5. Неподвижные точки функциональных программ
- 49:08Семинар 5. Переписывание термов. Симплификатор Isabelle
- 01:23:25Лекция 6. Существование наименьшей неподвижной точки. Вычисление значения неподвижной точки на конкретных данных
- 01:11:55Семинар 6. Объявление типов в Isabelle/HOL. Рекурсивные функции. Индукция
- 01:25:36Лекция 7. Верификация распределенных систем. Задача вычисления произведения матриц
- 01:01:34Семинар 7. Индуктивные отношения. Язык структурированных доказательств Isar
- 01:40:02Лекция 8. Пример верификации распределенной программы (умножение двух матриц)
- 01:08:07Семинар 8. Язык структурированных доказательств Isar (продолжение)
- 01:25:11Лекция 9. Теория процессов. Понятие процесса. Операции над процессами. Эквивалентность процессов
- 01:13:13Семинар 9. Механизм локалей в Isabelle. Примеры практического применения инструмента
- 01:22:35Лекция 10. Бимоделирование. Критерий сильной эквивалентности процессов. Наблюдаемая эквивалентность
- 01:25:50Лекция 11. Наблюдаемая эквивалентность. Планировщик процессов (пример)
- 01:22:15Лекция 12. Формальная модель криптографических протоколов. Протокол Yaholom