There is contention between the "European school" of language design, who prefer LL-based grammars, and the "US-school", who predominantly prefer LR-based grammars. This is largely due to teaching traditions and the detailed description of specific methods and tools in certain text books; another influence may be Niklaus Wirth at ETH Zürich in Switzerland, whose research has described a number of ways of optimising LL(1) languages and compilers.

LL parser article in wikipedia.

Удаление ложных путей в 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.

Goanna: синтаксический model checker

Goanna использует model checking для обнаружения дефектов, зависящих от потока управления, таких как: утечки памяти, использование неинициализированной переменной, возможное разыменование нулевого указателя. Атомарные предикаты формируются путем поиска по шаблону конструкций выделения, использования и освобождения ресурса p.

В статье [1] приводится пример формулы CTL для описания корректной работы с памятью:

AG(malloc_p => AG(free_p => !EF used_p))

Кстати, на мой взгляд в формуле есть ошибка в темпоральном операторе перед предикатом free_p.

Для обнаружения ошибок типа переполнения буфера используется интервальный анализ (на основе абстрактной интерпретации). Простые циклы анализируются без использования техники расширения (widening).

Для уменьшения числа ложных обнаружений используется статический анализ контр-примера. По результатам этого анализа строится автомат-наблюдатель (observer automaton), который в дальнейшем используется для удаления ложных путей. Выполняется проверка синхронного произведения автоматов-наблюдателей и исходной модели программы. Процесс уточнения повторяется до тех пор пока перестают обнаруживаться новые дефекты и перестают удаляться ложные пути.

[1] A. Fehnker, J. Brauer, R. Huuck, S. Seefried Goanna: Syntactic Software Model Checking //
6th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2008 Seoul, Korea.