Легковесный метод для поиска состояний гонок.

Авторы

Андрианов Павел, Мутилин Вадим, Хорошилов Алексей

Аннотация

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

Полный текст статьи в формате pdf (на английском)

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

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

Издание

Сборник трудов Весеннего/Летнего коллоквиума молодых ученых по программной инженерии. ИСП РАН, 2014. сс. 27-33.

DOI: 10.15514/SYRCOSE-2014-8-4

978-5-91474-020-4

Научная группа

Технологии программирования

Все публикации за 2014 год

Все публикации