In this work we present Goanna, the first tool that uses an off-the-shelf model checker for the static analysis of C/C++ source
code. We outline its architecture and show how syntactic properties can be expressed in CTL. Once the properties have been
defined the tool analyses source code automatically and efficiently. We demonstrate its applicability by presenting experimental
results on analysing OpenSSL and the GNU coreutils.