На пути к автоматизированной локализации ошибок в C программах с циклами

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