Введение
Глава 1. Обзор работ в области моделирования памяти Си-программ в инструментах статической верификации 13
1.1. Обзор методов и инструментов статической верификации 13
1.2. Использование решателей логических формул в теориях в инструментах статической верификации 23
1.3. Актуальность задачи статической верификации Си-программ 27
1.4. Теории, поддерживаемые современными решателями 30
1.5. Проблемы моделирования семантики языка Си 31
1.6. Моделирование памяти Си-программ 35
1.7. Выводы 74
Глава 2. Проблемы существующих моделей памяти для языка Си 78
2.1. Использование инструментов автоматической статической верификации Си-программ в проекте LDV 78
2.2. Проблемы существующих моделей памяти для инструментов автоматической статической верификации Си-программ 83
2.3. Использование инструментов дедуктивной верификации в проекте Astraver 84
2.4. Цель и задачи работы 89
Глава 3. Модель для ограниченных областей памяти на основе теории неинтерпретируемых функций 91
3.1. Обзор предлагаемого метода 91
3.2. Описание метода 95
3.3. Оптимизации 107
3.4. Результаты 109
3.5. Выводы 113
Глава 4. Модель памяти с вложенными регионами для дедуктивной верификации 117
4.1. Базовый язык с поддержкой вложенности 118
4.2. Нормализация Си-программ 129
4.3. Модельная семантика базового языка 134
4.4. Анализ регионов для базового языка с поддержкой вложенности153
4.5. Выводы 161
Заключение 164
Список литературы
