Irina Shoshmina

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

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

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

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

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

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

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

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

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

Модальности

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

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

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

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

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

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

Базисы CTL

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Основные компоненты аксиоматической теории

Необходимость формализации математических доказательств

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

Условные выполнимость и выводимость

Свойства аксиоматических теорий

Аксиоматическая теория Гильберта исчисления высказываний

Свойства аксиоматической теории Гильберта исчисления высказываний

Разница между тестированием и верификацией

Постановка задачи верификации программ

Верикация - метод обеспечения качества программ

Слабейшее предусловие для оператора присваивания

Частичная и тотальная корректность программы

Проблема построения слабейшего предусловия

Сильнейшее постусловие программы

Доказательство корректности ациклических программ

Индуктивный метод Флойда

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

Особенности метода резолюции в логике предикатов

Категорические силлогизмы Аристотеля

Предваренная нормальная форма

"Правильные" и "неправильные" умозаключения в логике предикатов

Сколемовская форма формул логики предикатов

Унификация атомарных предикатов

Постановка задачи логического вывода в логике предикатов

Примеры с методом резолюций в логике предикатов

Пациенты и знахари

Силлогизм Barbara и бурундукотигр

Пара задач с математическими объектами

Парадокс Эпименида

Мир вампуса и метод резолюции в логике предикатов

Структура программы на ПРОЛОГе

Запрос к базе данных и метод резолюции

Несколько программ на ПРОЛОГе

Программа определения родства на ПРОЛОГе

Формализация информации с помощью логики предикатов

Синтаксис логики предикатов

Разбор структуры предикатной формулы

Ограниченность логики высказываний при формализации объектов реального мира

Использование логики предикатов в примерах

Семантика логики предикатов

Определение эквивалентности (равносильности) формул логики предикатов

Примеры эквивалентных преобразований формул логики предикатов

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

Общезначимые и невыполнимые формулы в логике предикатов

Определение ограниченных кванторов

Примеры формализации с использованием ограниченных кванторов

Эквивалентные преобразования с ограниченными кванторами

Закон о продаже оружия и ограниченные кванторы

Мир вампуса и ограниченные кванторы

Математические определения и ограниченные кванторы

Кванторы и область их действия

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

Методы решения задачи SAT

Частные случаи задачи SAT

Когда логический вывод "не работает"?

Проблема адекватности формализации на примере задачи Кислера

Проверка "правильности" схемы умозаключения по таблице истинности

Силлогизмы и "новое знание"

Тривиальные и неправильные схемы умозаключений

Задача Порецкого о птицах - пример задачи с 4-мя переменными

Основная теорема логического вывода

Проверка "правильности" схемы умозаключения через КНФ или ДНФ

Формулировка основной теоремы логического вывода через невыполнимую формулу

Использование метода резолюций в логике высказываний

Метод резолюции в логике высказываний. Основные понятия

Непротиворечивость и полнота метода резолюций в логике высказываний

Хорновские дизъюнкты в примере из химии

Интерпретация резолютивного вывода в логике высказываний на естественном языке

Формулировка проблемы выполнимости SAT

Практические задачи как задачи SAT