DOI: 10.17587/prin.16.558-569

УДК: 004.45

Исследование значимости элементов трасс ошибок в статической верификации программного обеспечения

В. О. Мордань¹, канд. физ.-мат. наук, науч. сотр., mordan@ispras.ru, B. С. Мутилин^1,2, канд. физ.-мат. наук, науч. сотр., mutilin@ispras.ru,
¹ Институт системного программирования им. В. П. Иванникова Российской академии наук, Москва
² Московский физико-технический институт (национальный исследовательский университет), Долгопрудный

Рассмотрено одно из ключевых ограничений верификации программного обеспечения — необходимость ручной оценки результатов, включающих предупреждения о потенциальных ошибках. Такие предупреждения должны быть либо исправлены, либо классифицированы как ложные срабатывания, что требует участия экспертов. Для решения описанной проблемы формально введено понятие тщательности трасс ошибок в верификации программного обеспечения. Тщательность трасс оценивается на основе результатов инструментальных средств, участвовавших в соревнованиях по верификации программного обеспечения SV-COMP, что демонстрирует практическое применение предлагаемого подхода к реальным верификационным задачам. Показано, как понятие тщательности может быть использовано в качестве метрики при сравнении инструментальных средств верификации, а также для улучшения автоматического подтверждения результатов верификации. Помимо этого, предложенная метрика показывает, какие именно элементы трассы ошибки понадобятся для ее визуализации.

Ключевые слова: верификация программного обеспечения, тщательность, результаты верификации, валидация, трасса ошибки

Стр. 558—569

Ссылка для цитирования:
Мордань В. О., Мутилин В. С. Исследование значимости элементов трасс ошибок в статической верификации программного обеспечения // Программная инженерия. 2025. Том 16, № 11. C. 558—569. DOI: 10.17587/prin.16.558-569.

Полный текст на eLIBRARY