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


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

Авторы

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

Аннотация

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

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

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

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

Издание

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

DOI: 10.15514/SYRCOSE-2014-8-4

978-5-91474-020-4

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

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

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