Goanna: Syntactic Software Model Checking

Goanna is an industrial-strength static analysis tool used in academia and industry alike to find bugs in C/C++ programs. Unlike existing approaches Goanna uses the off-the-shelf NuSMV model checker as its core analysis engine on a syntactic flow-sensitive program abstraction. The CTL-based model checking approach enables a high degree of flexibility in writing checks, scales to large number of checks, and can scale to large code bases. Moreover, the tool incorporates techniques from constraint solving, classical data flow analysis and a CEGAR inspired counterexample based path reduction. In this paper we describe Goanna's core technology, its features and the relevant techniques, as well as our experiences of using Goanna on large code bases such as the Firefox web browser.

• Type: Conference
• Year: 2008
• Where: ATVA
• Authors: Ralf Huuck, Ansgar Fehnker, Sean Seefried, Jörg Brauer
• Keywords: ATVA 2008, Goanna, Goanna's Core Technology, Hardware, Large Code Bases