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

Цель исследования - разработка методов и инструментов статического и динамического анализа, позволяющих находить дефекты проектирования и реализации приложений, критические дефекты и уязвимости, дефекты производительности программ, проявляющиеся на современных параллельных архитектурах. Разработан метод формализации ошибочных ситуаций при статическом анализе программ в ходе символьного выполнения, предлагающий ряд способов описать искомую ошибочную ситуацию с разной степенью точности. Разработан метод поиска дефектов переполнения буфера в программах на языках Си/Си++, основанный на некоторых из предложенных формализаций ошибочных ситуаций. Метод реализован в инструменте статического анализа Svace, разрабатываемого в ИСП РАН, и показал хорошее качество при тестировании на исходном коде операционной системы Android 5.