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.