Goanna: Syntactic Software Model Checking

Ralf Huuck, Ansgar Fehnker, Sean Seefried, Jörg Brauer

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis
Subtitle of host publication6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings
EditorsSung Deok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, Mahesh Viswanathan
Place of PublicationBerlin
PublisherSpringer
Pages216-221
Number of pages6
ISBN (Electronic)978-3-540-88387-6
ISBN (Print)978-3-540-88386-9
DOIs
Publication statusPublished - 2008
Externally publishedYes
Event6th International Symposium Automated Technology for Verification and Analysis 2008 - Seoul, Korea, Republic of
Duration: 20 Oct 200823 Oct 2008
Conference number: 6

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume5311
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference6th International Symposium Automated Technology for Verification and Analysis 2008
Abbreviated titleATVA 2008
CountryKorea, Republic of
CitySeoul
Period20/10/0823/10/08

Keywords

  • Model Check
  • Interval Analysis
  • Static Analysis Tool
  • Interval Constraint
  • Path Reduction

Fingerprint Dive into the research topics of 'Goanna: Syntactic Software Model Checking'. Together they form a unique fingerprint.

  • Cite this

    Huuck, R., Fehnker, A., Seefried, S., & Brauer, J. (2008). Goanna: Syntactic Software Model Checking. In S. D. Cha, J-Y. Choi, M. Kim, I. Lee, & M. Viswanathan (Eds.), Automated Technology for Verification and Analysis: 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings (pp. 216-221). (Lecture Notes in Computer Science; Vol. 5311). Berlin: Springer. https://doi.org/10.1007/978-3-540-88387-6_17