Software Model Checking and Goanna

We are frequently asked whether Goanna is a software model checker. After all, we analyse software and use a model checker to do so. However, while Goanna uses a model checker in the background for part of its analysis, it is not a software model checker. In the typical meaning of the word.

Software model checkers build a full model that captures all the details of the language, in our case C/C++. Which can be a difficult task, especially for C/C++ programs. Defining the semantics of the C/C++ language alone can already be a momentous task. This is the main reason why many software model checkers restrict themselves to a subset of C, often a subset of ANSI C. It may not be the most common dialect of C used in practice, but it is reasonably well documented and understood.

Goanna in contrast build models that include, depending on the checked property, only information on the occurrence of relevant variables, pointers, statements, expressions, etc. This allows us to consider all of the most common dialects of C/C++. Goanna thus uses an abstraction – to use a technical term – that is unlike any abstractions you see in software model checking. The difference? Speed. While software model checkers can analyse software very thoroughly, they cannot compete with static code analysis tools on speed. Goanna can.

No Comments

Post a Comment