Skip to main content

An abstract specification language for static program analysis

Authors

Michael Vistein, Frank Ortmeier, Wolfgang Reif, Ralf Huuck and Ansgar Fehnker

Universitaet Augsburg

NICTA

Abstract

Static program analysers typically come with a set of hard-coded checks, leaving little room for the user to add additional properties. In this work, we present a uniform approach to enable the speci cation of new static analysis checks in a concise manner. In particular, we present our GPSL/GXSL language to defi ne new control flow checks. The language is closely related to CTL speci cations that are combined with XPath queries. Moreover, we provide a number of speci cations as implemented in our tool Goanna, and report on our experiences of adding new checks.

BibTeX Entry

  @inproceedings{Vistein_ORHF_09,
    author           = {Vistein, Michael and Ortmeier, Frank and Reif, Wolfgang and Huuck, Ralf and Fehnker, Ansgar},
    month            = nov,
    year             = {2009},
    keywords         = {static analysis, specification language, ctl, xpath},
    address          = {Germany},
    title            = {An Abstract Specification Language for Static Program Analysis},
    booktitle        = {Systems Software Verification}
  }

Download

Served by Apache on Linux on seL4.