Верификация Си-программ: объяснение условий корректности и стандартная библиотека

Представлены два направления развития проекта по верификации Си-программ, разрабатываемого в ИСИ СО РАН. Во-первых, аксиоматическая семантика языка C-kernel была расширена семантической разметкой. Метки, выводимые непосредственно исчислением Хоара, соответствуют различным аспектам условий корректности (УК). Эти метки могут быть извлечены из термов и преобразованы в пояснения на естественном языке. Пояснения, понятные обычному пользователю системы верификации, могут быть полезны для понимания УК и локализации ошибок. Во-вторых, было специфицировано подмножество стандартной библиотеки языка Си. Спецификации написаны на языке ACSL и соответствуют модели памяти языка C-light. В работе представлены примеры использования этих двух подходов.