Удаление ложных путей в Goanna

Для заданного контр-примера строится система уравнений интервального анализа. Если наименьшее решение является пустым множеством, то анализируемый контр-пример считается ложным.

В отличии от CEGAR, использующего SAT-решатели, и от подхода на основе аппроксимации многогранниками, предлагаемый в [1] подход имеет меньшие вычислительные затраты.

Формальной моделью является размеченная система переходов LTS (S, S0, A, R, F), являющаяся конечным автоматом над конечными словами.

Вводится понятие интервального автомата:
IA = (L, l0, X, E, update), где L - множество позиций в исходном коде, I0 - начальная позиция, X - множество интервальных переменных, E - множество дуг (определено на L * L), update - функция эффекта (E -> X * C(X)), C(X) - множество выражений над X.

Для интервального автомата определяется функция означивания v: X -> I.

Интервальному автомату P соответствует размеченная система переходов LTS(P) = (S, S0, A, R, F), где S равно множеству пар (l, v), где l - позиция в исходном коде, v - функция означивания. S0 - равно (l0. [-inf, inf]), A - подмножество E, R = S * A * S - множество кортежей вида ((l1, v1), (l1, l2), (l2, v2)). для переходов (l1, l2) из E, таких что v2 = v1[lhs(e) <- [rhsexpr(e)]_v1] и [rhsexpr(e)]_v2 не пусто; F = S.

Построенный автомат принимает только такие слова, которые соответствуют системам интервальных уравнений с непустым решением. Слова, которые соответствуют системам уравнений с пустым решением называются конфликтами.

Программе соответствует интервальный автомат LTS(P). Так как интервальные автоматы имеют бесконечное число состояний, используется конечная аппроксимация P^. Для заданного автомата P = (L, l0, X, E, update) строится абстракция P^ = (L, l0, E, E', L). где E' = {(l1, (l1, l2), l2) | (l1,l2) in E} - отношение переходов. В статье [1] описан итеративный алгоритм уточнения абстракций.

[1] A. Fehnker, R. Huuck, S. Seefried Counterexample Guided Path Reduction for Static Program Analysis // In the Festschrift of Correctness, Concurrency, and Compositionality for Willem-Paul de Roever, Kiel, Germany, 2008.