Goanna - a static model checker

Ansgar Fehnker; Ralf Huuck; Patrick Jayet; Michel Lussenburg; Felix Rauch

doi:10.1007/978-3-540-70952-7_20

Goanna - a static model checker

Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg, Felix Rauch

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

15 Citations (Scopus)

Abstract

In this work we present Goanna, the first tool that uses an off-the-shelf model checker for the static analysis of C/C++ source code. We outline its architecture and show how syntactic properties can be expressed in CTL. Once the properties have been defined the tool analyses source code automatically and efficiently. We demonstrate its applicability by presenting experimental results on analysing OpenSSL and the GNU coreutils.

Original language	English
Title of host publication	Formal Methods: Applications and Technology
Subtitle of host publication	11th International Workshop, FMICS 2006 and 5th International Workshop, PDMC 2006 Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers
Editors	Lubos Brim, Boudewijn R. Haverkort, Martin Leucker, Jaco van de Pol
Place of Publication	Berlin
Publisher	Springer, Springer Nature
Pages	297-300
Number of pages	4
ISBN (Print)	9783540709510, 3540709517
DOIs	https://doi.org/10.1007/978-3-540-70952-7_20
Publication status	Published - 2007
Externally published	Yes
Event	11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006 - Bonn, Germany Duration: 26 Aug 2006 → 27 Aug 2006

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4346
ISSN (Print)	0302-9743

Conference

Conference	11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006
Country/Territory	Germany
City	Bonn
Period	26/08/06 → 27/08/06

Access to Document

10.1007/978-3-540-70952-7_20

Cite this

Fehnker, A., Huuck, R., Jayet, P., Lussenburg, M., & Rauch, F. (2007). Goanna - a static model checker. In L. Brim, B. R. Haverkort, M. Leucker, & J. V. D. Pol (Eds.), Formal Methods: Applications and Technology: 11th International Workshop, FMICS 2006 and 5th International Workshop, PDMC 2006 Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers (pp. 297-300). (Lecture Notes in Computer Science; Vol. 4346). Springer, Springer Nature. https://doi.org/10.1007/978-3-540-70952-7_20

Fehnker, Ansgar ; Huuck, Ralf ; Jayet, Patrick et al. / Goanna - a static model checker. Formal Methods: Applications and Technology: 11th International Workshop, FMICS 2006 and 5th International Workshop, PDMC 2006 Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers. editor / Lubos Brim ; Boudewijn R. Haverkort ; Martin Leucker ; Jaco van de Pol. Berlin : Springer, Springer Nature, 2007. pp. 297-300 (Lecture Notes in Computer Science).

@inproceedings{e5492eca6e514783bfde5e3b80e34342,

title = "Goanna - a static model checker",

abstract = "In this work we present Goanna, the first tool that uses an off-the-shelf model checker for the static analysis of C/C++ source code. We outline its architecture and show how syntactic properties can be expressed in CTL. Once the properties have been defined the tool analyses source code automatically and efficiently. We demonstrate its applicability by presenting experimental results on analysing OpenSSL and the GNU coreutils.",

author = "Ansgar Fehnker and Ralf Huuck and Patrick Jayet and Michel Lussenburg and Felix Rauch",

year = "2007",

doi = "10.1007/978-3-540-70952-7_20",

language = "English",

isbn = "9783540709510",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Springer Nature",

pages = "297--300",

editor = "Lubos Brim and Haverkort, {Boudewijn R.} and Martin Leucker and Pol, {Jaco van de}",

booktitle = "Formal Methods: Applications and Technology",

address = "United States",

note = "11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006 ; Conference date: 26-08-2006 Through 27-08-2006",

}

Fehnker, A, Huuck, R, Jayet, P, Lussenburg, M & Rauch, F 2007, Goanna - a static model checker. in L Brim, BR Haverkort, M Leucker & JVD Pol (eds), Formal Methods: Applications and Technology: 11th International Workshop, FMICS 2006 and 5th International Workshop, PDMC 2006 Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers. Lecture Notes in Computer Science, vol. 4346, Springer, Springer Nature, Berlin, pp. 297-300, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, Bonn, North Rhine-Westphalia, Germany, 26/08/06. https://doi.org/10.1007/978-3-540-70952-7_20

Goanna - a static model checker. / Fehnker, Ansgar; Huuck, Ralf; Jayet, Patrick et al.
Formal Methods: Applications and Technology: 11th International Workshop, FMICS 2006 and 5th International Workshop, PDMC 2006 Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers. ed. / Lubos Brim; Boudewijn R. Haverkort; Martin Leucker; Jaco van de Pol. Berlin: Springer, Springer Nature, 2007. p. 297-300 (Lecture Notes in Computer Science; Vol. 4346).

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

TY - GEN

T1 - Goanna - a static model checker

AU - Fehnker, Ansgar

AU - Huuck, Ralf

AU - Jayet, Patrick

AU - Lussenburg, Michel

AU - Rauch, Felix

PY - 2007

Y1 - 2007

N2 - In this work we present Goanna, the first tool that uses an off-the-shelf model checker for the static analysis of C/C++ source code. We outline its architecture and show how syntactic properties can be expressed in CTL. Once the properties have been defined the tool analyses source code automatically and efficiently. We demonstrate its applicability by presenting experimental results on analysing OpenSSL and the GNU coreutils.

AB - In this work we present Goanna, the first tool that uses an off-the-shelf model checker for the static analysis of C/C++ source code. We outline its architecture and show how syntactic properties can be expressed in CTL. Once the properties have been defined the tool analyses source code automatically and efficiently. We demonstrate its applicability by presenting experimental results on analysing OpenSSL and the GNU coreutils.

U2 - 10.1007/978-3-540-70952-7_20

DO - 10.1007/978-3-540-70952-7_20

M3 - Conference proceeding contribution

SN - 9783540709510

SN - 3540709517

T3 - Lecture Notes in Computer Science

SP - 297

EP - 300

BT - Formal Methods: Applications and Technology

A2 - Brim, Lubos

A2 - Haverkort, Boudewijn R.

A2 - Leucker, Martin

A2 - Pol, Jaco van de

PB - Springer, Springer Nature

CY - Berlin

T2 - 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006

Y2 - 26 August 2006 through 27 August 2006

ER -

Fehnker A, Huuck R, Jayet P, Lussenburg M, Rauch F. Goanna - a static model checker. In Brim L, Haverkort BR, Leucker M, Pol JVD, editors, Formal Methods: Applications and Technology: 11th International Workshop, FMICS 2006 and 5th International Workshop, PDMC 2006 Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers. Berlin: Springer, Springer Nature. 2007. p. 297-300. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-70952-7_20

Goanna - a static model checker

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this