Irina Shoshmina

Программная реализация конечных автоматов

CTL - логика ветвящегося времени

CTL. Базовые операторы

Структура Крипке

Время: линейное или ветвящееся?

Семантика формул LTL

Выражение свойств систем в LTL

Модальности

ВременнАя логика

Линейная темпоральная логика. Синтаксис

Требования, зависящие от времени

Идея алгоритма проверки модели для CTL

Проверка модели CTL-формул

Семантика CTL формул

Базисы CTL

Алгоритм маркировки состояний подформулами CTL II

Алгоритм маркировки состояний подформулами CTL I

Проверка корректности системы управления микроволновой печью

Резюме по методу проверки модели для CTL

Пример проверки выполнимости формулы CTL

Символьные алгоритмы проверки выполнимости темпоральных формул

Идея компиляции структуры Крипке по программе

BDD vs взрыв числа состояний при верификации

Представление структуры Крипке с помощью BDD

Примеры верификации программ в Политехе

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

Общая характеристика достижений метода проверки модели

Слабейшее предусловие программы

Аксиоматический метод верификации программ А. Хоара

О сложности дедуктивной верификации

Инварианты циклов в задачах о вагонах и хамелеонах

Инварианты в вычислительных программах

Задача о кофейных зернах и игры со спичками

Разработка программ корректных по построению

Инварианты цикла

Метод Флойда и тестирование

Реагирующие системы

Задача о голландском флаге

Параллелизм - источник сложности анализа реагирующих систем

Программа как система переходов

Интерливинг в параллельных программах

Проблема взаимно исключающего доступа

Финансовые потери от программных ошибок

О проблеме корректности программных систем управления

Несет ли программист ответственность за человеческие жизни?

Метод проверки модели

Трудность доказательства корректности реагирующих систем

Примеры аксиоматических теорий