Генератор условий проверки - Verification condition generator

А генератор условий проверки является частым компонентом автоматизированного верификатор программы который синтезирует формальные условия проверки путем анализа исходного кода программы с использованием метода, основанного на Логика Хоара. Генераторы VC могут потребовать, чтобы исходный код содержал логические аннотации, предоставленные программистом или компилятором, такие как предварительные / постусловия и инварианты цикла (форма код подтверждения ). Генераторы VC часто сочетаются с Решатели SMT в бэкэнде верификатора программы. После того, как генератор условий проверки создал условия проверки, они передаются в автоматическое доказательство теорем, который затем может формально доказать правильность кода.

Были предложены методы использования операционная семантика машинных языков для автоматического создания генераторов условий проверки.^[1]

Рекомендации

1. Джон Мэтьюз; Дж. Стротер Мур; Сандип Рэй; Дарон Врун (2005). «Генерация условия проверки с помощью доказательства теорем». В Мики Херманн; Андрей Воронков (ред.). Proc. Int. Конф. Логика программирования, искусственного интеллекта и рассуждений. LNCS. 4246. Springer. С. 362–376.