В процессе написания программ разработчики часто совершают рефакторинги, изменяя структуру программ с сохранением их поведения. Однако существующие утилиты для автоматизации рефакторингов ненадежны, а ошибки, внесенные ими в программы, могут оставаться незамеченными. Доклад обосновывает применимость формальных методов для верификации корректности утилит для рефакторинга кода на языке C, при которой рефакторинг описывается на языке Coq с использованием формальной семантики из компилятора CompCert, а после машинной проверки доказательств из описания автоматически экстрагируется код утилиты для рефакторинга. Описывается proof-of-concept верифицированная реализация добавления и удаления локальной переменной в программах на языке C.
Жирков И. (науч. рук. Дергачев А.М.) Формальная верификация рефакторингов языка C // Сборник тезисов докладов конгресса молодых ученых. Электронное издание. – СПб: Университет ИТМО, [2023]. URL: https://kmu.itmo.ru/digests/article/11770