Введение
Глава 1. Способы формализации ограничений и модели программы для их проверки 10
1.1. Используемая терминология 13
1.2. Методы формализации и записи ограничений 24
1.3. Модели и представления программ для проверки ограничений 32
1.4. Алгоритмы статического анализа для проверки ограничений 35
1.5. Сравнительный обзор существующих статических анализаторов 40
Глава 2. Построение модели программы и её памяти 43
2.1. Модель программы 43
2.2. Операторы на ААСГ 49
2.3. Модель памяти 50
Глава 3. Формализация ограничений 71
3.1. Предикатная модель ограничений 71
3.2. Примеры формализации 75
3.3. Классификация ограничений 78
Глава 4. Алгоритмы статического анализа и их реализация в инфраструктуре Clang 87
4.1. Особенности реализованного подмножества правил 88
4.2. Этапы работы и особенности реализации анализатора 89
4.3. Разработанные алгоритмы анализа 98
4.4. Межмодульные алгоритмы 102
4.5. Результаты тестирования анализатора 103
Заключение 110
Список публикаций 112
Литература 113
