An Abstract Specification Language for Static Program Analysis

Michael Vistein; Frank Ortmeier; Wolfgang Reif; Ralf Huuck; Ansgar Fehnker

doi:10.1016/j.entcs.2009.09.066

An Abstract Specification Language for Static Program Analysis

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

Research output: Contribution to journal › Article › Academic › peer-review

3 Citations (Scopus)

37 Downloads (Pure)

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 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.

Original language	English
Pages (from-to)	181-197
Number of pages	17
Journal	Electronic notes in theoretical computer science
Volume	254
DOIs	https://doi.org/10.1016/j.entcs.2009.09.066
Publication status	Published - 2009
Externally published	Yes

Access to Document

10.1016/j.entcs.2009.09.066Licence: CC BY-NC-ND

Vistein2019specificationFinal published version, 368 KBLicence: CC BY-NC-ND

Cite this

@article{bc4b47ed330e4f2e981f426679d49f1f,

title = "An Abstract Specification Language for Static Program Analysis",

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 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.",

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

year = "2009",

doi = "10.1016/j.entcs.2009.09.066",

language = "English",

volume = "254",

pages = "181--197",

journal = "Electronic notes in theoretical computer science",

issn = "1571-0661",

publisher = "Elsevier",

}

TY - JOUR

T1 - An Abstract Specification Language for Static Program Analysis

AU - Vistein, Michael

AU - Ortmeier, Frank

AU - Reif, Wolfgang

AU - Huuck, Ralf

AU - Fehnker, Ansgar

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

U2 - 10.1016/j.entcs.2009.09.066

DO - 10.1016/j.entcs.2009.09.066

M3 - Article

SN - 1571-0661

VL - 254

SP - 181

EP - 197

JO - Electronic notes in theoretical computer science

JF - Electronic notes in theoretical computer science

ER -