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

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