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