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

Fingerprint

Model checking
Syntactics
Data flow analysis
Core analysis
Web browsers
Static analysis
Engines
Industry

Keywords

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

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
Huuck, Ralf ; Fehnker, Ansgar ; Seefried, Sean ; Brauer, Jörg. / Goanna : Syntactic Software Model Checking. Automated Technology for Verification and Analysis: 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings. editor / Sung Deok Cha ; Jin-Young Choi ; Moonzoo Kim ; Insup Lee ; Mahesh Viswanathan. Berlin : Springer, 2008. pp. 216-221 (Lecture Notes in Computer Science).
@inproceedings{a548c8d265d6488d99cc637411840ceb,
title = "Goanna: Syntactic Software Model Checking",
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",
author = "Ralf Huuck and Ansgar Fehnker and Sean Seefried and J{\"o}rg Brauer",
year = "2008",
doi = "10.1007/978-3-540-88387-6_17",
language = "English",
isbn = "978-3-540-88386-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "216--221",
editor = "Cha, {Sung Deok} and Jin-Young Choi and Moonzoo Kim and Insup Lee and Mahesh Viswanathan",
booktitle = "Automated Technology for Verification and Analysis",

}

Huuck, R, Fehnker, A, Seefried, S & Brauer, J 2008, Goanna: Syntactic Software Model Checking. in SD 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. Lecture Notes in Computer Science, vol. 5311, Springer, Berlin, pp. 216-221, 6th International Symposium Automated Technology for Verification and Analysis 2008, Seoul, Korea, Republic of, 20/10/08. https://doi.org/10.1007/978-3-540-88387-6_17

Goanna : Syntactic Software Model Checking. / Huuck, Ralf; Fehnker, Ansgar ; Seefried, Sean; Brauer, Jörg.

Automated Technology for Verification and Analysis: 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings. ed. / Sung Deok Cha; Jin-Young Choi; Moonzoo Kim; Insup Lee; Mahesh Viswanathan. Berlin : Springer, 2008. p. 216-221 (Lecture Notes in Computer Science; Vol. 5311).

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

TY - GEN

T1 - Goanna

T2 - Syntactic Software Model Checking

AU - Huuck, Ralf

AU - Fehnker, Ansgar

AU - Seefried, Sean

AU - Brauer, Jörg

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

KW - Model Check

KW - Interval Analysis

KW - Static Analysis Tool

KW - Interval Constraint

KW - Path Reduction

U2 - 10.1007/978-3-540-88387-6_17

DO - 10.1007/978-3-540-88387-6_17

M3 - Conference contribution

SN - 978-3-540-88386-9

T3 - Lecture Notes in Computer Science

SP - 216

EP - 221

BT - Automated Technology for Verification and Analysis

A2 - Cha, Sung Deok

A2 - Choi, Jin-Young

A2 - Kim, Moonzoo

A2 - Lee, Insup

A2 - Viswanathan, Mahesh

PB - Springer

CY - Berlin

ER -

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