Irina Shoshmina

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

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

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

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

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

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

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

Модальности

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

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

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

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

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

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

Базисы CTL

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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