Аннотация доклада.

В докладе рассматривается задача разработки эффективных алгоритмов статического анализа программ на языке С с целью выявления некорректных операций с памятью. Одним из аспектов ее решения является разработка языка промежуточного представления программ для трансляции в него исходной программы и написания аннотаций. Другим аспектом решения задачи является создание математической модели, позволяющей обосновать корректность применяемого алгоритма анализа.