Верификация C-программ на основе смешанной аксиоматической семантики

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