Skip to main content

An abstract specification language for static program analysis


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

Universitaet Augsburg



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

    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}


Served by Apache on Linux on seL4.