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. https://doi.org/10.1016/j.entcs.2009.09.060