Поиск состояний гонок1
- Поддержка примитивов синхронизации для атомарного доступа.
- Поддержка модели прерываний.
- Чувствительный к путям анализ разделяемых данных с уточнением.
- Анализ взаимодействия потоков с помощью сообщений.
- Воспроизведение полного пути к ошибке с переключениями.
- Анализ алиасов в многопоточном случае.
- Валидация результатов поиска гонок на основе известных исправлений ошибок в ядре ОС Linux.
- Проверка свойств безопасности памяти с помощью символических графов памяти в модульном многопоточном анализе.
- Поиск высокоуровневых гонок.
- Поиск состояний гонок, приводящих к использованию памяти после освобождения и использованию неинициализированной памяти.
Верификация программ1
- Выявление и построение моделей окружения по трассам динамического выполнения (Runtime leaning of environment models).
- Методы верификации и сбора данных об архитектурных сущностях в системах реального времени (ARINC-совместимых) с помощью предикатного анализа.
- Эвристическая модель памяти на основе регионов для анализа явных значений.
- Методы визуализации доказательств корректности программ.
- Моделирование памяти с разбиением на регионы с использованием теории массивов.
- Абстракция итераций циклов и их итеративное уточнение.
- Обнаружение неопределенного поведения для программ на языке С при помощи символьных графов памяти
- Приоритизация селекции локальных путей в анализе с запоминанием абстракций.
- Моделирование памяти по требованию для анализа при помощи предикатных абстракций.
Методы формальной верификации в применении к крупным программным системам3
- Автоматизация извлечения знаний о поведении окружения целевых компонентов крупных программных систем для их формальной верификации при помощи машинного обучения, мониторинга и/или статического анализа исходного кода.
- Автоматизация определения шаблонов использования внешних интерфейсов для верификации компонентов крупных программных систем при помощи машинного обучения, мониторинга и/или статического анализа исходного кода.
- Разработка языка предметной области для моделирования поведения окружения компонентов крупных программных систем.
- Оптимизация алгоритмов планирования системы масштабируемой автоматической верификации (в том числе методами машинного обучения).
- Разработка интерактивной системы помощи инженеру-верификатору для решения трудных задач верификации на основе анализа результатов верификации исходного кода программ.
Развитие методов и инструментов дедуктивной верификации программ на языке Си2
- Полнота метода генерации условий верификации и системы рамочных правил переписывания для логики путей и динамических фреймов.
- Полная система рамочных правил (переписывания) для теории списков в логике путей и динамических фреймов.
- Полнота и корректность метода трансляции структурных программ с произвольным использованием опертора goto в монадическое представление (state-монада с явным счетчиком текущей инструкции, то есть с явным состоянием текущей метки).
- Обратимая процедура разрешения перегруженных констант с помощью итеративного вывода типов и сопоставления с образцами высших порядков (higher order pattern).
- Формальное доказательство корректности опреации переинтерпретации типа области памяти в высокоуровневой типищированной модели (в Isabelle/HOL).
- Формальное доказтельство корректности флгоритма приближенного ограниченного E-матчинга (сопоставления с образцом в теории конгруэнтности) (уже есть доказательство завершимости инстанцирования и реализация алгоритма).
Развитие технологий SMT-солверов3
- Сравнение показателей производительности SMT-солверов на промышленных задачах в зависимости от выбранных параметров стратегии поиска решений.
- Поддержка теории множеств в SMT-солверах.
Формальные методы тестирования программ (протоколов) на основе конечно-автоматных моделей4
- Построение спецификации программных компонент в виде:
- конечного автомата (FSM);
- расширенного конечного автомата (EFSM);
- временного конечного автомата.
- Синтез тестов с гарантированной полнотой
1к.ф.-м.н. Вадим Мутилин
2к.ф.-м.н. Михаил Мандрыкин
3к.ф.-м.н. Алексей Хорошилов
4д.ф.-м.н. Нина Владимировна Евтушенко