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