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

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

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

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

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

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

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

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

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

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

1к.ф.-м.н. Вадим Мутилин
2к.ф.-м.н. Илья Захаров
3к.ф.-м.н. Михаил Мандрыкин
4к.ф.-м.н. Алексей Хорошилов