Skip to main content

TS

GoannaSMT — a static analyzer with SMT-based refinement

Authors

Mark Bradley, Franck Cassez, Ansgar Fehnker, Thomas Given-Wilson, Ralf Huuck and Maximillian Junker

NICTA

UNSW

TU Munich

Abstract

We present an industrial strength static analysis tool for automated bug detection in C/C++ source code called GoannaSMT. The underlying technology of GoannaSMT is an automata-based approach to static analysis, where high-level syntactic source code abstractions are subjected to a custom-built explicit state model checker. Resulting error traces are then subjected to an SMT solver in a path-refinement loop for closer inspection of their feasibility. As a result GoannaSMT is highly precise while at the same time scaling to millions of lines of code. We present the core technology, architecture, and experiences.

BibTeX Entry

  @misc{Bradley_CFGHJ_12,
    publisher        = {ENTCS},
    author           = {Bradley, Mark and Cassez, Franck and Fehnker, Ansgar and Given-Wilson, Thomas and Huuck, Ralf and
                        Junker, Maximillian},
    month            = jul,
    year             = {2012},
    keywords         = {smt solving, refinement, static analysis, model checking, tools, c/c++},
    title            = {{GoannaSMT} --- A Static Analyzer with {SMT}-based Refinement},
    booktitle        = {Tools for Automatic Program AnalysiS (TAPAS 2012)},
    pages            = {??},
    address          = {Deauville, France}
  }

Download

Served by Apache on Linux on seL4.