Goanna: Syntactic Software Model Checking

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

doi:10.1007/978-3-540-88387-6_17

Goanna: Syntactic Software Model Checking

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

12 Citations (Scopus)

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 language	English
Title of host publication	Automated Technology for Verification and Analysis
Subtitle of host publication	6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings
Editors	Sung Deok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, Mahesh Viswanathan
Place of Publication	Berlin
Publisher	Springer
Pages	216-221
Number of pages	6
ISBN (Electronic)	978-3-540-88387-6
ISBN (Print)	978-3-540-88386-9
DOIs	https://doi.org/10.1007/978-3-540-88387-6_17
Publication status	Published - 2008
Externally published	Yes
Event	6th International Symposium Automated Technology for Verification and Analysis 2008 - Seoul, Korea, Republic of Duration: 20 Oct 2008 → 23 Oct 2008 Conference number: 6

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	5311
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	6th International Symposium Automated Technology for Verification and Analysis 2008
Abbreviated title	ATVA 2008
Country/Territory	Korea, Republic of
City	Seoul
Period	20/10/08 → 23/10/08

Keywords

Model Check
Interval Analysis
Static Analysis Tool
Interval Constraint
Path Reduction

Access to Document

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

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). Springer. https://doi.org/10.1007/978-3-540-88387-6_17

Huuck, Ralf ; Fehnker, Ansgar ; Seefried, Sean et al. / 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{\textquoteright}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",

address = "Germany",

note = "6th International Symposium Automated Technology for Verification and Analysis 2008, ATVA 2008 ; Conference date: 20-10-2008 Through 23-10-2008",

}

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 et al.
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 proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Goanna

T2 - 6th International Symposium Automated Technology for Verification and Analysis 2008

AU - Huuck, Ralf

AU - Fehnker, Ansgar

AU - Seefried, Sean

AU - Brauer, Jörg

N1 - Conference code: 6

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

Y2 - 20 October 2008 through 23 October 2008

ER -

Huuck R, Fehnker A, Seefried S, Brauer J. Goanna: Syntactic Software Model Checking. In Cha SD, Choi JY, 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). doi: 10.1007/978-3-540-88387-6_17

Goanna: Syntactic Software Model Checking

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this