Верификация финитной итерации над массивами с выходом из цикла в Си программах

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