An Abstract Specification Language for Static Program Analysis

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

Research output: Contribution to journalArticleAcademicpeer-review

3 Citations (Scopus)
9 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 languageEnglish
Pages (from-to)181-197
Number of pages17
JournalElectronic notes in theoretical computer science
Volume254
DOIs
Publication statusPublished - 2009
Externally publishedYes

Fingerprint

Specification languages
Program Analysis
Specification Languages
Static Analysis
Specification
Specifications
XPath
Static analysis
Flow Control
Flow control
Query
Language

Cite this

Vistein, Michael ; Ortmeier, Frank ; Reif, Wolfgang ; Huuck, Ralf ; Fehnker, Ansgar. / An Abstract Specification Language for Static Program Analysis. In: Electronic notes in theoretical computer science. 2009 ; Vol. 254. pp. 181-197.
@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",

}

An Abstract Specification Language for Static Program Analysis. / Vistein, Michael; Ortmeier, Frank; Reif, Wolfgang; Huuck, Ralf; Fehnker, Ansgar.

In: Electronic notes in theoretical computer science, Vol. 254, 2009, p. 181-197.

Research output: Contribution to journalArticleAcademicpeer-review

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

VL - 254

SP - 181

EP - 197

JO - Electronic notes in theoretical computer science

JF - Electronic notes in theoretical computer science

SN - 1571-0661

ER -