Advertisement

Goanna: Syntactic Software Model Checking

  • Ralf Huuck
  • Ansgar Fehnker
  • Sean Seefried
  • Jörg Brauer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)

Abstract

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.

Keywords

Model Check Interval Analysis Static Analysis Tool Interval Constraint Path Reduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232–244 (2004)Google Scholar
  4. 4.
    Emanuelsson, P., Nilsson, U.: A comparative study of industrial static analysis tools. Electronic notes in theoretical computer science (2008)Google Scholar
  5. 5.
    Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: Proc. Symposium on Operating Systems Design and Implementation, San Diego, CA (October 2000)Google Scholar
  6. 6.
    Henzinger, T., Jhala, R., Majumdar, R., SUTRE, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    scan.coverity.com: Open source report. Technical report, Coverity Inc (2008)Google Scholar
  9. 9.
    Fehnker, A., Huuck, R., Jayet, P., Lussenburg, M., Rauch, F.: Model checking software at compile time. In: Proc. TASE 2007. IEEE Computer Society Press, Los Alamitos (2007)Google Scholar
  10. 10.
    Holzmann, G.: Static source code checking for user-defined properties. In: Proc. IDPT 2002, Pasadena, CA, USA (June 2002)Google Scholar
  11. 11.
    Dams, D., Namjoshi, K.: Orion: High-precision methods for static error analysis of C and C++ programs. Bell Labs Tech. Mem. ITD-04-45263Z, Lucent Technologies (2004)Google Scholar
  12. 12.
    Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 351–380. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas, pp. 269–282. ACM Press, New York (1979)CrossRefGoogle Scholar
  14. 14.
    Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 300–315. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    Fehnker, A., Huuck, R., Seefried, S.: Counterexample guided path reduction for static program analysis. In: Correctness, Concurrency, and Compositionality. Volume number to be assigned of Festschrift Series, LNCS. Springer, Heidelberg (2008)Google Scholar
  16. 16.
    Andersen, L.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, Unversity of Copenhagen (1994)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Ralf Huuck
    • 1
  • Ansgar Fehnker
    • 1
  • Sean Seefried
    • 1
  • Jörg Brauer
    • 1
  1. 1.National ICT Australia Ltd. (NICTA) Locked Bag 6016University of New South WalesSydneyAustralia

Personalised recommendations