Goanna — A Static Model Checker. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 6 articles , 1 standard article )

Showing results 1 to 6 of 6.
Sorted by year (citations)

  1. Brauer, Jörg; King, Andy; Kowalewski, Stefan: Abstract interpretation of microcontroller code: intervals meet congruences (2013)
  2. Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Counterexample guided path reduction for static program analysis (2010)
  3. Peleska, Jan: Integrated and automated abstract interpretation, verification and testing of C/C++ modules (2010)
  4. Fehnker, Ansgar; Huuck, Ralf; Schlich, Bastian; Tapp, Michael: Automatic bug detection in microcontroller software by static program analysis (2009) ioport
  5. Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Incremental false path elimination for static software analysis (2009)
  6. Huuck, Ralf; Fehnker, Ansgar; Seefried, Sean; Brauer, Jörg: Goanna: Syntactic software model checking (2008) ioport