- Об институте
- Инновации
- Структура
- Отдел "Архитектуры вычислительных систем"
- Отдел "Информационных систем"
- Отдел "Компиляторных технологий"
- Отдел "Системного программирования"
- Отдел "Системной интеграции и прикладных программных комплексов"
- Отдел "Теоретической информатики"
- Отдел "Технологий программирования"
- Ученый совет
- Диссертационный совет
- Центр верификации ОС Linux
- Исследовательский центр доверенного искусственного интеллекта
- Центр компетенции по параллельным и распределенным вычислениям
- Образование
- Издания
- Новости
- Лицензии
Об одной системе вывода, связанной со статическим анализом программ.
Авторы
Захаров В.А., Викторова М.С.
Аннотация
В работе предпринята попытка применить метод логики потоков к решению задачи статического анализа программ. Основная идея предложенного подхода состоит в том, чтобы разделить задачу анализа программы на два этапа. На первом этапе осуществляется логический вывод системы ограничений, которым должны удовлетворять вычисляемые инвариантные соотношения, а на втором этапе для решения образованной системы соотношений применяются итеративные алгоритмы. Построена система логического вывода инвариантных соотношений для задачи определения инициализированности переменных и доказана ее полнота.
Ключевые слова
статический анализ программ, логика потоков, система ограничений, логический вывод
Издание
Труды V Международной конференции «Дискретные модели в теории управляющих систем», (Ратмино, 26-29 мая 2003 г.), 2003, МАКС-Пресс - МГУ Москва, с. 26-29.