Дедуктивная верификация программ ¹,²,³

• Модель неограниченных указателей и блочно-байтовая модель памяти с переинтерпретацией.
• Моделирование функциональных указателей с помощью теории доменов.
• Реализация автоматического построения моделей кода функций из промежуточного представления Frama-C.
• Формализация семантики функций выделения памяти.
• Разработка специфического алгоритма сопоставления с образцом для правил элаборации в логике высшего порядка.
• Автоматический вывод триггеров, упорядочение и группировка лемм для их предварительного конечного инстанцирования.
• Генерация операций и соответствующих семантических правил для выделения и освобождения локальных регионов памяти.
• Генерация семантических правил для интерпретации областей памяти как объектов разных типов.
• Генерация семантических правил и правил элаборации для инициализаторов объектов композитных типов.

Детали по этому направлению см. здесь.

Автоматическая статическая верификация ²,³

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

• Поддержка примитивов синхронизации для атомарного доступа в предикатном анализе.
• Поддержка модели прерываний в инструменте CPALockator (поддержка непрерывных регионов с точки зрения эффектов).
• Воспроизведение полного пути к ошибке с переключениями в подходе модульного анализа многопоточных программ.
• Анализ алиасов в многопоточном случае.
• Валидация результатов поиска гонок на основе известных исправлений ошибок в ядре ОС Linux.
• Анализ взаимодействия потоков с помощью сообщений.
• Поиск высокоуровневых гонок.
• Поиск состояний гонок, приводящих к использованию памяти после освобождения и использованию неинициализированной памяти. С расширением множества отслеживаемых событий в thread-modular подходе (например, помечать free для поиска ошибок типа use-after-free).

Верификация безопасности использования памяти

• Проверка свойств безопасности памяти с помощью символьных графов памяти в модульном многопоточном анализе.
• Комбинирование символьных графов памяти с произвольными числовыми и предикатными доменами.
• Верификация программ с циклами с использованием анализа индуктивных переменных на графе потока управления.
• Моделирование памяти по требованию для анализа при помощи предикатных абстракций.
• Моделирование памяти с разбиением на регионы с использованием теории массивов.
• Оптимизация сравнения состояний памяти в операторе останова SMG с помощью ИИ.
• Выбор порядка обхода состояний программы на основе метрик сложности.

Верификация общих правил и система верификации Klever

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

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

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

Динамический анализ ²,³

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

• Поддержка нескольких точек ожидания в рамках одной итерации.
• Поддержка композиции точек ожидания в инструменте поиска гонок RaceHunter.
• Реализация критерия покрытия на основе алиасов памяти для многопоточных программ.
• Уменьшение потребления оперативной памяти в алгоритме мониторинга событий во фреймворке для динамического обнаружения гонок по данным RaceHunter.
• Распараллеливание алгоритмов в методе обнаружения гонок по данным RaceHunter.
• Интеграция фреймворка для обнаружения гонок по данным RaceHunter в ядро операционной системы Linux.

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

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

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