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 contribution › Academic › 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
Publisher	Springer
Pages	297-300
Number of pages	4
ISBN (Electronic)	978-3-540-70952-7
ISBN (Print)	978-3-540-70951-0
DOIs	https://doi.org/10.1007/978-3-540-70952-7_20
Publication status	Published - 2006
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 Conference number: 11

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4346

Workshop

Workshop	11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006
Abbreviated title	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. (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 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. 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",

address = "Germany",

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

}

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › 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

N1 - Conference code: 11

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

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. Springer. 2006. 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

Workshop

Access to Document

Fingerprint

Cite this