Поиск состояний гонок¹

• Поддержка примитивов синхронизации для атомарного доступа.
• Поддержка модели прерываний.
• Чувствительный к путям анализ разделяемых данных с уточнением.
• Анализ взаимодействия потоков с помощью сообщений.
• Воспроизведение полного пути к ошибке с переключениями.
• Анализ алиасов в многопоточном случае.
• Валидация результатов поиска гонок на основе известных исправлений ошибок в ядре ОС Linux.
• Проверка свойств безопасности памяти с помощью символических графов памяти в модульном многопоточном анализе.
• Поиск высокоуровневых гонок.
• Поиск состояний гонок, приводящих к использованию памяти после освобождения и использованию неинициализированной памяти.

Верификация программ¹

• Выявление и построение моделей окружения по трассам динамического выполнения (Runtime leaning of environment models).
• Методы верификации и сбора данных об архитектурных сущностях в системах реального времени (ARINC-совместимых) с помощью предикатного анализа.
• Эвристическая модель памяти на основе регионов для анализа явных значений.
• Методы визуализации доказательств корректности программ.
• Моделирование памяти с разбиением на регионы с использованием теории массивов.
• Абстракция итераций циклов и их итеративное уточнение.
• Обнаружение неопределенного поведения для программ на языке С при помощи символьных графов памяти
• Приоритизация селекции локальных путей в анализе с запоминанием абстракций.
• Моделирование памяти по требованию для анализа при помощи предикатных абстракций.

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

• Автоматизация извлечения знаний о поведении окружения целевых компонентов крупных программных систем для их формальной верификации при помощи машинного обучения, мониторинга и/или статического анализа исходного кода.
• Автоматизация определения шаблонов использования внешних интерфейсов для верификации компонентов крупных программных систем при помощи машинного обучения, мониторинга и/или статического анализа исходного кода.
• Разработка языка предметной области для моделирования поведения окружения компонентов крупных программных систем.
• Оптимизация алгоритмов планирования системы масштабируемой автоматической верификации (в том числе методами машинного обучения).
• Разработка интерактивной системы помощи инженеру-верификатору для решения трудных задач верификации на основе анализа результатов верификации исходного кода программ.

Развитие методов и инструментов дедуктивной верификации программ на языке Си²

• Полнота метода генерации условий верификации и системы рамочных правил переписывания для логики путей и динамических фреймов.
• Полная система рамочных правил (переписывания) для теории списков в логике путей и динамических фреймов.
• Полнота и корректность метода трансляции структурных программ с произвольным использованием опертора goto в монадическое представление (state-монада с явным счетчиком текущей инструкции, то есть с явным состоянием текущей метки).
• Обратимая процедура разрешения перегруженных констант с помощью итеративного вывода типов и сопоставления с образцами высших порядков (higher order pattern).
• Формальное доказательство корректности опреации переинтерпретации типа области памяти в высокоуровневой типищированной модели (в Isabelle/HOL).
• Формальное доказтельство корректности флгоритма приближенного ограниченного E-матчинга (сопоставления с образцом в теории конгруэнтности) (уже есть доказательство завершимости инстанцирования и реализация алгоритма).

Развитие технологий SMT-солверов³

• Сравнение показателей производительности SMT-солверов на промышленных задачах в зависимости от выбранных параметров стратегии поиска решений.
• Поддержка теории множеств в SMT-солверах.

Формальные методы тестирования программ (протоколов) на основе конечно-автоматных моделей⁴

• Построение спецификации программных компонент в виде:
  1. конечного автомата (FSM);
  2. расширенного конечного автомата (EFSM);
  3. временного конечного автомата.
• Синтез тестов с гарантированной полнотой

¹к.ф.-м.н. Вадим Мутилин
²к.ф.-м.н. Михаил Мандрыкин
³к.ф.-м.н. Алексей Хорошилов
⁴д.ф.-м.н. Нина Владимировна Евтушенко