Interprocedural Pointer Analysis in Goanna

Citations of this article
Mendeley users who have this article in their library.


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 model checker NuSMV 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 and scales to large code bases. In this paper, a new approach to pointer analysis for C is described. It is detailed how this technique is integrated into the model checking approach in order to perform interprocedural analysis. The performance and precision of this approach are demonstrated using a case study. © 2009 Elsevier B.V. All rights reserved.




Brauer, J., Huuck, R., & Schlich, B. (2009). Interprocedural Pointer Analysis in Goanna. Electronic Notes in Theoretical Computer Science, 254, 65–83.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free