Кошелев, Владимир Константинович Межпроцедурный статический анализ для поиска ошибок в исходном коде программ на языке C#

brief description

Кошелев, Владимир Константинович Межпроцедурный статический анализ для поиска ошибок в исходном коде программ на языке C#
ОГЛАВЛЕНИЕ ДИССЕРТАЦИИ
кандидат наук Кошелев, Владимир Константинович
Оглавление

Стр.

Введение

Глава 1. Методы поиска ошибок в исходном коде

1.1 Задачи статического анализа

1.2 Дефекты в исходном коде

1.3 Методы статического анализа

1.3.1 Задача точного поиска дефектов

1.3.2 Абстрактная интерператция

1.3.3 Метод CEGAR

1.3.4 Сведение к выполнимости формул

1.3.5 Нестрогий анализ

1.3.6 Инструмент Saturn

1.3.7 Промышленные статические анализаторы

1.3.8 Существующие анализаторы программ на языке С#

1.3.9 Инструмент статического анализа Svace

Глава 2. Внутреннее представление для языка С#

2.1 Особенности анализа языка С#

2.2 Описание внутреннего представления

Глава 3. Внутрипроцедурный анализ

3.1 Символьное выполнение

3.2 Развертка графа потока управления

3.3 Объединение состояний

3.4 Оптимизация предикатов

3.5 Поддержка циклов с фиксированным числом итераций

Глава 4. Межпроцедурный анализ

4.1 Построение резюме

4.2 Вспомогательные части резюме

4.3 Применения резюме

Стр.

4.4 Поддержка чистых методов и массивов

4.5 Организация анализа помеченных данных

Глава 5. Поиск дефектов

5.1 Символьное выполнение для поиска ошибок

5.2 Определения ошибочных ситуаций

5.3 Примеры множеств абстракций

5.4 Примеры поиска ошибок при помощи предложенных абстракций

5.5 Поиск ошибок по определению на примере обращения к

нулевому указателю

5.5.1 Реализация поиска доступа к null

5.5.2 Межпроцедурный анализ доступа к null

5.6 Утечка ресурсов

5.6.1 Постановка задачи

5.6.2 Условие утечки

5.6.3 Связанные ресурсы

5.6.4 Момент утечки

5.6.5 Объединение символьных состояний

5.6.6 Поиск утечки ресурсов по критерию ошибки

5.7 Влияние нестрогости предложенного анализа на поиск ошибок

Глава 6. Инструмент SharpChecker

6.1 Описание инструмента

6.2 Порядок анализа

6.3 Построение графа вызовов

6.4 Построение графа потока управления

6.5 Резюме для внешних методов

6.6 Использование SMT-решателей

6.7 Результаты

Заключение

Список литературы