Invariant elimination of definite iterations over arrays in C programs verification

Данная работа представляет дальнейшее развитие метода верификации финитной итерации [7]. Он расширяет метод смешанной аксиоматической семантики [1], предложенный для верификации C-light программ. Это расширение включает метод верификации для финитной итерации над неизменяемыми массивами с выходом из цикла в C-light программах. Метод содержит правило вывода для итерации без инвариантов, которое использует специальную функцию, выражающую действие тела цикла. Данное правило было реализовано в генераторе условий корректности, являющемся частью нашей системы верификации C-light программ. Для доказательства порождённых условий корректности применяется метод математической индукции, вызывающий сложности у SMT-решателей. В нашей системе верификации на стадии доказательства используется SMT-решатель CVC4. Для преодоления упомянутой трудности применяется стратегия переписывания условий корректности. Для доказательства условий корректности предложен метод, основанный на расширении теории новыми теоремами. Рассмотрен пример, иллюстрирующий применение данных методов. Статья публикуется в авторской редакции.