An Abstract Specification Language for Static Programm Analysis

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

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 specification of new static analysis checks in a concise manner. In particular, we present our GPSL/GXSL language to define new control flow checks. The language is closely related to CTL specifications that are combined with XPath queries. Moreover, we provide a number of specifications as implemented in our tool Goanna, and report on our experiences of adding new checks.
Proceedings of the 4th International Workshop on Systems Software Verification (SSV 2009)

Publisher: Elsevier B.V.

DOI: 10.1016/j.entcs.2009.09.066