Методы формальной верификации программ

Программа курса находится в стадии изменения

Преподаватель: TBD

Темы курса

  • Моделирование параллельных систем
    • Синхронизация параллельных программ
    • Представление первого порядка. Степень детализация переходов
  • Классическая логика и формальные теории (исчисления)
    • Логика высказываний, логика предикатов. Исчисление высказываний. Исчисление предикатов.
    • Формальная арифметика. Непротиворечивость формальной арифметики.
    • Теорема Генцена.
    • Теорема Гёделя о неполноте.
  • Темпоральные логики
    • Логика деревьев вычислений CTL*.
    • Логика линейного времени(LTL). Логика ветвящегося времени(CTL).
    • Справедливость.
  • Проверка на основе моделей
    • Верификация. Верификация моделей для CTL. Табличная верификация моделей для LTL. Верификация моделей для CTL*.
    • Двоичные разрешающие диаграммы. Представление булевых функции. Представление моделей Крипке.
    • Символьная верификация моделей. Представление неподвижной точки. Условия справедливости. Синтез OBDD. Разделенная нормальная форма для логики линейного времени LTL.
    • Верификация моделей и теория автоматов. Автомат Бюхи. Проверка пустоты. Трансляция LTL в автоматы. Верификация моделей на лету. Символьная проверка вложенности языков. Редукция частичных порядков. Композиционные доказательства. Абстракция: редукция по конусу влияния, абстракция данных.
  • Дедуктивная верификация
    • Алгоритмическая логика Хоара. Слабейшие предусловия, сильнейшие постусловия, полная и частичная корректность.
    • Дедуктивная верификация параллельных систем. Логика Owicki-Gries. Композиционный метод Rely-Guarantee. Взаимодействующие последовательные процессы Хоара.
    • Сепарационная логика. Сепарационная логика для одновременно исполняющихся процессов.
    • RGSep, SAGL, Local Rely-Guarantee, Deny-Guarantee Reasoning и другие логики для дедуктивной верификации, построенные на основе синтеза композиционного метода с сепарационной логикой.