An Abstract Specification Language for Static Program Analysis
Michael Vistein, Frank Ortmeier, Wolfgang Reif, Ralf Huuck, Ansgar Fehnker · Electronic Notes in Theoretical Computer Science · 2009
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.