Goanna - A Static Model Checker

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

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

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 languageEnglish
Title of host publicationFormal Methods: Applications and Technology
Subtitle of host publication11th International Workshop, FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006, Revised Selected Papers
EditorsLubos Brim, Boudewijn R. Haverkort, Martin Leucker, Jaco van de Pol
PublisherSpringer
Pages297-300
Number of pages4
ISBN (Electronic)978-3-540-70952-7
ISBN (Print)978-3-540-70951-0
DOIs
Publication statusPublished - 2006
Externally publishedYes
Event11th International Workshop on Formal Methods for Industrial Critical Systems - Bonn, Germany
Duration: 26 Aug 200627 Aug 2006
Conference number: 11

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume4346

Workshop

Workshop11th International Workshop on Formal Methods for Industrial Critical Systems
Abbreviated titleFMICS 2006
CountryGermany
CityBonn
Period26/08/0627/08/06

Fingerprint

Static analysis
Syntactics

Cite this

Fehnker, A., Huuck, R., Jayet, P., Lussenburg, M., & Rauch, F. (2006). 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. https://doi.org/10.1007/978-3-540-70952-7_20
Fehnker, Ansgar ; Huuck, Ralf ; Jayet, Patrick ; Lussenburg, Michel ; Rauch, Felix. / 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. Springer, 2006. pp. 297-300 (Lecture Notes in Computer Science).
@inproceedings{abb8f8a4cbe240f88f5cf08b36db53b1,
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 = "2006",
doi = "10.1007/978-3-540-70952-7_20",
language = "English",
isbn = "978-3-540-70951-0",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "297--300",
editor = "Lubos Brim and Haverkort, {Boudewijn R.} and Martin Leucker and Pol, {Jaco van de}",
booktitle = "Formal Methods: Applications and Technology",

}

Fehnker, A, Huuck, R, Jayet, P, Lussenburg, M & Rauch, F 2006, 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, pp. 297-300, 11th International Workshop on Formal Methods for Industrial Critical Systems, Bonn, 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; Lussenburg, Michel; Rauch, Felix.

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. Springer, 2006. p. 297-300 (Lecture Notes in Computer Science; Vol. 4346).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 - 2006

Y1 - 2006

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 contribution

SN - 978-3-540-70951-0

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

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. Springer. 2006. p. 297-300. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-70952-7_20