Сборники трудов ИСП РАН


Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux.

М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.В. Хорошилов.

Аннотация

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

Ключевые слова

верификация, статический анализ, драйвер устройства, операционная система Linux

Издание

Труды Института системного программирования РАН, том 22, 2012, стр. 293-326.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2012-22-17

Полный текст статьи в формате pdf Вернуться к содержанию тома