Комплексный подход к локализации ошибок при верификации Си-программ

Отличительной чертой проекта C-light является максимальное использование формальных непротиворечивых методов. Это касается не только фундаментальных базисов для верификации, таких как операционная семантика Плоткина или логика Хоара, но и реализационных аспектов. Одним из таких моментов является локализация потенциальных ошибок. В большинстве известных систем верификации локализация ошибок просто реализуется программистами как часть функционала системы без подведения какой-либо формальной основы под этот процесс. В свете недавнего расширения проекта C-light техникой семантической разметки и выбора инструментария LLVM/Clang для входного блока системы мы приводим обзор наших наработок для решения этой задачи.