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

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

Язык:
Русский
Аннотация: 
Отличительной чертой проекта C-light является максимальное использование формальных непротиворечивых методов. Это касается не только фундаментальных базисов для верификации, таких как операционная семантика Плоткина или логика Хоара, но и реализационных аспектов. Одним из таких моментов является локализация потенциальных ошибок. В большинстве известных систем верификации локализация ошибок просто реализуется программистами как часть функционала системы без подведения какой-либо формальной основы под этот процесс. В свете недавнего расширения проекта C-light техникой семантической разметки и выбора инструментария LLVM/Clang для входного блока системы мы приводим обзор наших наработок для решения этой задачи.
УДК: 
Страницы: 
79-96
Файл: 
Номер: