Goanna: What’s Different and Why Model Checking?
So what’s different about Goanna and why did we approach the static analysis challenge with model checking?
In case you weren’t aware; Goanna is the first static analysis tool to implement model checking after 4 years research at NICTA (National ICT Australia), which is Australia’s leading ICT government research organisation.
The result is that the key attributes for Goanna’s differences are as follows;
Speed– Goanna builds a model of the source code which is stored persistently and then queried, as opposed to running checking algorithms, so its fast and often only requires a few seconds;
Recall– is high as Goanna covers all paths simultaneously, rather than sequentially unfurling selected combinations for checking. Goanna also currently provides 30+ classes of checks and will include even more in future releases;
Scalability – is excellent as we use an internal module for defining new check queries. Yes, we do intend to productize this for user defined checks in the near future, yet that’s a separate road-map post. This also means that we do not [overly – there will always be some trade off] compromise speed and recall with larger code bases, and additionally Goanna can review large code bases on an incremental change basis;
Precision– means keeping the false positive count low, and Goanna does this as its model is comprehensive and the queries are highly targeted. Goanna’s queries target bugs (we prefer this word to “defects”) not coding style or syntax, so the noise level remains very low.
The balance of model checking across these attributes provides the uniqueness that is Goanna. Its why Goanna can be made available within the IDE, so that we assist you in bringing higher quality software to market faster; without changing the way that you work.
And that’s why we called it Goanna; native to Australia, blends in with its environment and eats bugs.